{"action":"closed","issue":{"url":"https://api.github.com/repos/mpreiner/bugzilla_migration_test/issues/131","repository_url":"https://api.github.com/repos/mpreiner/bugzilla_migration_test","labels_url":"https://api.github.com/repos/mpreiner/bugzilla_migration_test/issues/131/labels{/name}","comments_url":"https://api.github.com/repos/mpreiner/bugzilla_migration_test/issues/131/comments","events_url":"https://api.github.com/repos/mpreiner/bugzilla_migration_test/issues/131/events","html_url":"https://github.com/mpreiner/bugzilla_migration_test/issues/131","id":250772350,"number":131,"title":"more regressions (Bugzilla #744)","user":{"login":"mpreiner","id":4653598,"avatar_url":"https://avatars0.githubusercontent.com/u/4653598?v=4","gravatar_id":"","url":"https://api.github.com/users/mpreiner","html_url":"https://github.com/mpreiner","followers_url":"https://api.github.com/users/mpreiner/followers","following_url":"https://api.github.com/users/mpreiner/following{/other_user}","gists_url":"https://api.github.com/users/mpreiner/gists{/gist_id}","starred_url":"https://api.github.com/users/mpreiner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mpreiner/subscriptions","organizations_url":"https://api.github.com/users/mpreiner/orgs","repos_url":"https://api.github.com/users/mpreiner/repos","events_url":"https://api.github.com/users/mpreiner/events{/privacy}","received_events_url":"https://api.github.com/users/mpreiner/received_events","type":"User","site_admin":false},"labels":[{"id":668716808,"url":"https://api.github.com/repos/mpreiner/bugzilla_migration_test/labels/enhancement","name":"enhancement","color":"84b6eb","default":true}],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/mpreiner/bugzilla_migration_test/milestones/11","html_url":"https://github.com/mpreiner/bugzilla_migration_test/milestone/11","labels_url":"https://api.github.com/repos/mpreiner/bugzilla_migration_test/milestones/11/labels","id":2705864,"number":11,"title":"1.6","description":"","creator":{"login":"mpreiner","id":4653598,"avatar_url":"https://avatars0.githubusercontent.com/u/4653598?v=4","gravatar_id":"","url":"https://api.github.com/users/mpreiner","html_url":"https://github.com/mpreiner","followers_url":"https://api.github.com/users/mpreiner/followers","following_url":"https://api.github.com/users/mpreiner/following{/other_user}","gists_url":"https://api.github.com/users/mpreiner/gists{/gist_id}","starred_url":"https://api.github.com/users/mpreiner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mpreiner/subscriptions","organizations_url":"https://api.github.com/users/mpreiner/orgs","repos_url":"https://api.github.com/users/mpreiner/repos","events_url":"https://api.github.com/users/mpreiner/events{/privacy}","received_events_url":"https://api.github.com/users/mpreiner/received_events","type":"User","site_admin":false},"open_issues":0,"closed_issues":18,"state":"open","created_at":"2017-08-16T21:05:41Z","updated_at":"2017-08-16T23:42:46Z","due_on":null,"closed_at":null},"comments":0,"created_at":"2017-08-16T21:58:07Z","updated_at":"2017-08-16T23:42:46Z","closed_at":"2017-08-16T23:42:46Z","body":"**Imported from Bugzilla**\nReporter: *Florian Schanda*\nStatus: *NEW*\nSeverity: *enhancement*\nAssigned to: *Andrew Reynolds*\nComponent: *{Internals} SMT Engine*\nMilestone: *1.6*\nVersion: *master*\nPlatform: *All*\nOS: *All*\n\nOriginal attachment names and IDs:\n- _[a.smt2](http://cvc4.cs.stanford.edu/bugzilla3//attachment.cgi?id=374)_ (1 of 3 regressions, ID 374)\n- _[b.smt2](http://cvc4.cs.stanford.edu/bugzilla3//attachment.cgi?id=375)_ (2 of 3 regressions, ID 375)\n- _[c.smt2](http://cvc4.cs.stanford.edu/bugzilla3//attachment.cgi?id=376)_ (3 of 3 regressions, ID 376)\n\nOn 2016-07-05 05:54:54 -0700, Florian Schanda wrote:\n> Hi, I will attach three verification conditions that all used to go through\n> in a reasonable time (a few seconds) but now do not.\n> \n> Known good revision: SHA: 26b8cc7f672d580dfc7355dac1c4352a3c7c32e8\n> Known bad revision: SHA: 9b9e41478d0e1e62fa4bc8ca206a70dff5e8c392\n> \n> Sorry its so old, but its from a bug report where the user used a shipped\n> version and now found this once they upgraded.\n> \n> Looking in the stats, most of the time is spent in the smt engine, so\n> I've submitted under that component.\n> \n> The third one may be different (much more time is spent in bv).\n\nOn 2016-07-05 05:55:41 -0700, Florian Schanda wrote:\n> Created attachment 374\n> 1 of 3 regressions\n\nOn 2016-07-05 05:55:57 -0700, Florian Schanda wrote:\n> Created attachment 375\n> 2 of 3 regressions\n\nOn 2016-07-05 05:56:13 -0700, Florian Schanda wrote:\n> Created attachment 376\n> 3 of 3 regressions\n\nOn 2016-07-05 06:29:55 -0700, Florian Schanda wrote:\n> I should note that we run with \\-\\-no\\-cbqi and this does affect the result.\n\nOn 2016-07-05 14:10:09 -0700, Andrew Reynolds wrote:\n> Hi Florian,\n> \n> I am getting that the current version of CVC4 solves each of these regressions with no command line parameters.\n> \n> If you use \\-\\-no\\-cbqi, CVC4 times out on each.\n> \n> Can you confirm?  I can look deeper into why the current cvc4 with \\-\\-no\\-cbqi times out, but just wanted to clarify this first.\n> \n> \\-Andy\n\nOn 2016-07-05 15:51:10 -0700, Florian Schanda wrote:\n> On Tuesday 05 Jul 2016 14:10:09 bugzilla@church.cims.nyu.edu wrote:\n> > If you use \\-\\-no\\-cbqi, CVC4 times out on each.\n> \n> Yes, we use \\-\\-no\\-cbqi in SPARK.\n> \n> \tFlorian\n\nOn 2016-07-05 17:17:22 -0700, Andrew Reynolds wrote:\n> (In reply to comment # 6)\n> > On Tuesday 05 Jul 2016 14:10:09 bugzilla@church.cims.nyu.edu wrote:\n> > > If you use \\-\\-no\\-cbqi, CVC4 times out on each.\n> > \n> > Yes, we use \\-\\-no\\-cbqi in SPARK.\n> > \n> \n> I know, I'm just noting that disabling this option allows CVC4 to solve these.\n> \n> \n> I tracked down the issue in these benchmarks (a/b/c.smt2) to a commit SHA: fd3844131f334e929bfb04eb2dcb6229cf1190cd on March 12 2016, which made CVC4 more robust with regards to how theory combination and quantifier instantiation are interleaved.  In the previous version, quantifier instantiation was unfair wrt theory combination. Resolving this issue has made CVC4 slower on these benchmarks.\n> \n> So at this point, to solve these, my suggestions are either to use one of these options:\n> \n> (1) [no command line parameters]\n> (2) \"\\-\\-no\\-cbqi \\-\\-no\\-inst\\-when\\-strict\\-interleave \\-\\-inst\\-when\\-phase=N\" for some N>=4\n> \n> \n> I'd definitely prefer if you didn't try to mimic the old version of CVC4 (option 2), since it was somewhat by luck that it was solving these fast.  \n> \n> As I recall, my suggestion to use \"\\-\\-no\\-cbqi\" was initially motivated by a single benchmark that you sent which CVC4 timed out on.  I'd prefer it perhaps if you did not use this option and we revisited why it was slow.  Btw, do you have any data on the overall impact of cvc4 with/without \"\\-\\-no\\-cbqi\"?\n> \n> Let me know what you think.\n> \n> \\-Andy\n> \n> \n> \n> \n> >     Florian\n\nOn 2016-07-11 08:21:51 -0700, Florian Schanda wrote:\n> On Tuesday 05 Jul 2016 17:17:22 bugzilla@church.cims.nyu.edu wrote:\n> > I know, I'm just noting that disabling this option allows CVC4 to solve\n> > these.\n> \n> Yep.\n> \n> > So at this point, to solve these, my suggestions are either to use one of\n> > these options:\n> > \n> > (1) [no command line parameters]\n> > (2) \"\\-\\-no\\-cbqi \\-\\-no\\-inst\\-when\\-strict\\-interleave \\-\\-inst\\-when\\-phase=N\" for\n> > some N>=4\n> \n> I will play with both, but (1) I know is bad for our testsuite.\n> \n> > I'd definitely prefer if you didn't try to mimic the old version of CVC4\n> > (option 2), since it was somewhat by luck that it was solving these fast.\n> \n> OK. I realize luck may always be a factor.\n> \n> > As I recall, my suggestion to use \"\\-\\-no\\-cbqi\" was initially motivated by a\n> > single benchmark that you sent which CVC4 timed out on.  I'd prefer it\n> > perhaps if you did not use this option and we revisited why it was slow. \n> > Btw, do you have any data on the overall impact of cvc4 with/without\n> > \"\\-\\-no\\-cbqi\"?\n> \n> Its one of many; I've raised bug 745 with a tarball of all 133 current \n> regressions between \\-\\-no\\-cbqi and no options.\n> \n> \tFlorian\n\nOn 2016-07-11 08:28:45 -0700, Andrew Reynolds wrote:\n> (In reply to comment # 8)\n> > On Tuesday 05 Jul 2016 17:17:22 bugzilla@church.cims.nyu.edu wrote:\n> > > I know, I'm just noting that disabling this option allows CVC4 to solve\n> > > these.\n> > \n> > Yep.\n> > \n> > > So at this point, to solve these, my suggestions are either to use one of\n> > > these options:\n> > > \n> > > (1) [no command line parameters]\n> > > (2) \"\\-\\-no\\-cbqi \\-\\-no\\-inst\\-when\\-strict\\-interleave \\-\\-inst\\-when\\-phase=N\" for\n> > > some N>=4\n> > \n> > I will play with both, but (1) I know is bad for our testsuite.\n> > \n> > > I'd definitely prefer if you didn't try to mimic the old version of CVC4\n> > > (option 2), since it was somewhat by luck that it was solving these fast.\n> > \n> > OK. I realize luck may always be a factor.\n> > \n> > > As I recall, my suggestion to use \"\\-\\-no\\-cbqi\" was initially motivated by a\n> > > single benchmark that you sent which CVC4 timed out on.  I'd prefer it\n> > > perhaps if you did not use this option and we revisited why it was slow. \n> > > Btw, do you have any data on the overall impact of cvc4 with/without\n> > > \"\\-\\-no\\-cbqi\"?\n> > \n> > Its one of many; I've raised bug 745 with a tarball of all 133 current \n> > regressions between \\-\\-no\\-cbqi and no options.\n> > \n> \n> Excellent, this should help, I'll take a look at these later this week...I'll be travelling until Wednesday.\n> \n> \\-Andy\n> \n> >     Florian\n\nOn 2016-07-11 08:46:06 -0700, Florian Schanda wrote:\n> On Monday 11 Jul 2016 08:28:46 bugzilla@church.cims.nyu.edu wrote:\n> > Excellent, this should help, I'll take a look at these later this\n> > week...I'll be travelling until Wednesday.\n> \n> I've also raised 746 for all regressions between an old version of CVC4 and \n> the current head (all under \\-\\-no\\-cbqi). I'll do another one without \\-\\-no\\-cbqi.\n> \n> Safe travels!\n\n"}}
{"actor":{"display_login":"mpreiner"}}