{"action":"opened","issue":{"url":"https://api.github.com/repos/CVC4/CVC4/issues/754","repository_url":"https://api.github.com/repos/CVC4/CVC4","labels_url":"https://api.github.com/repos/CVC4/CVC4/issues/754/labels{/name}","comments_url":"https://api.github.com/repos/CVC4/CVC4/issues/754/comments","events_url":"https://api.github.com/repos/CVC4/CVC4/issues/754/events","html_url":"https://github.com/CVC4/CVC4/issues/754","id":251395278,"number":754,"title":"Segmentation fault in parser (Bugzilla #535)","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":21411288,"url":"https://api.github.com/repos/CVC4/CVC4/labels/enhancement","name":"enhancement","color":"84b6eb","default":true}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-08-19T02:47:26Z","updated_at":"2017-08-19T02:47:26Z","closed_at":null,"body":"**Imported from Bugzilla**\nReporter: *Kshitij*\nStatus: *RESOLVED*\nSeverity: *enhancement*\nAssigned to: *Andrew Reynolds*\nComponent: *Quantifiers*\nMilestone: *---*\nVersion: *master*\nPlatform: *PC*\nOS: *Mac OS*\n\nOriginal attachment names and IDs:\n- _[concat_invariant_inductive.smt](http://cvc4.cs.stanford.edu/bugzilla_attachments/196_concat_invariant_inductive.smt)_ (sample benchmark, ID 196)\n- _[backtrace.txt](http://cvc4.cs.stanford.edu/bugzilla_attachments/197_backtrace.txt)_ (backtrace, ID 197)\n\nOn 2013-09-30 13:54:37 -0700, Kshitij wrote:\n> Created attachment 196\n> sample benchmark\n> \n> On the attached benchmark, in debug build we get the following:\n> \n> \n> \n> (error \"Parse Error: concat\\_invariant\\_inductive.smt:47.20: Assertion failure\n> CVC4::Expr CVC4::Expr::operator[](unsigned int) const\n> /home/kshitij/cvc/CVC4.CVC4/builds/x86\\_64\\-unknown\\-linux\\-gnu/debug/../../../src/expr/expr\\_template.cpp:290:\n> \n>   i >\\= 0 && i < d\\_node\\->getNumChildren()\n> Child index out of bounds\")\n> \n> \n> \n> \n> This happens during parsing. Along the backtrace is\n> \n> static bool isClosed(Expr e, std::set<Expr>& free, std::hash\\_set<Expr, ExprHashFunction>& closedCache)\n> \n> In this function, e.getKind() is CVC4::kind::FORALL\n> \n> Backtrace will be attached with next benchmark. I am filing this under quantifiers, but parser might be more appropriate \\-\\- Andy?\n\nOn 2013-09-30 13:57:10 -0700, Kshitij wrote:\n> Created attachment 197\n> backtrace\n\nOn 2013-10-01 12:32:38 -0700, Andrew Reynolds wrote:\n> This was a bug in the Smt2 parser, fixed in my latest commit.\n\n"}}
{"actor":{"display_login":"mpreiner"}}