{"action":"created","issue":{"url":"https://api.github.com/repos/CVC4/CVC4/issues/2002","repository_url":"https://api.github.com/repos/CVC4/CVC4","labels_url":"https://api.github.com/repos/CVC4/CVC4/issues/2002/labels{/name}","comments_url":"https://api.github.com/repos/CVC4/CVC4/issues/2002/comments","events_url":"https://api.github.com/repos/CVC4/CVC4/issues/2002/events","html_url":"https://github.com/CVC4/CVC4/issues/2002","id":327148925,"number":2002,"title":"Assertion failure in equality engine","user":{"login":"4tXJ7f","id":1926228,"avatar_url":"https://avatars3.githubusercontent.com/u/1926228?v=4","gravatar_id":"","url":"https://api.github.com/users/4tXJ7f","html_url":"https://github.com/4tXJ7f","followers_url":"https://api.github.com/users/4tXJ7f/followers","following_url":"https://api.github.com/users/4tXJ7f/following{/other_user}","gists_url":"https://api.github.com/users/4tXJ7f/gists{/gist_id}","starred_url":"https://api.github.com/users/4tXJ7f/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/4tXJ7f/subscriptions","organizations_url":"https://api.github.com/users/4tXJ7f/orgs","repos_url":"https://api.github.com/users/4tXJ7f/repos","events_url":"https://api.github.com/users/4tXJ7f/events{/privacy}","received_events_url":"https://api.github.com/users/4tXJ7f/received_events","type":"User","site_admin":false},"labels":[{"id":21411286,"url":"https://api.github.com/repos/CVC4/CVC4/labels/bug","name":"bug","color":"b60205","default":true},{"id":671891438,"url":"https://api.github.com/repos/CVC4/CVC4/labels/major","name":"major","color":"e99695","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-05-29T02:12:45Z","updated_at":"2018-05-29T02:27:54Z","closed_at":null,"author_association":"MEMBER","body":"On the incremental QF_ANIA/UltimateBuchiAutomizer/openbsd_cstpncpy-alloca_true-termination.c.i.smt2 benchmark, we get the following assertion failure (takes around 10 seconds):\r\n\r\n```\r\n(error \"Assertion failure.\r\nCVC4::TNode CVC4::theory::eq::EqualityEngine::getRepresentative(CVC4::TNode) const\r\n../../../../src/theory/uf/equality_engine.cpp:523:\r\n\r\n  hasTerm(t)\r\n\")\r\n```"},"comment":{"url":"https://api.github.com/repos/CVC4/CVC4/issues/comments/392635458","html_url":"https://github.com/CVC4/CVC4/issues/2002#issuecomment-392635458","issue_url":"https://api.github.com/repos/CVC4/CVC4/issues/2002","id":392635458,"user":{"login":"4tXJ7f","id":1926228,"avatar_url":"https://avatars3.githubusercontent.com/u/1926228?v=4","gravatar_id":"","url":"https://api.github.com/users/4tXJ7f","html_url":"https://github.com/4tXJ7f","followers_url":"https://api.github.com/users/4tXJ7f/followers","following_url":"https://api.github.com/users/4tXJ7f/following{/other_user}","gists_url":"https://api.github.com/users/4tXJ7f/gists{/gist_id}","starred_url":"https://api.github.com/users/4tXJ7f/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/4tXJ7f/subscriptions","organizations_url":"https://api.github.com/users/4tXJ7f/orgs","repos_url":"https://api.github.com/users/4tXJ7f/repos","events_url":"https://api.github.com/users/4tXJ7f/events{/privacy}","received_events_url":"https://api.github.com/users/4tXJ7f/received_events","type":"User","site_admin":false},"created_at":"2018-05-29T02:27:54Z","updated_at":"2018-05-29T02:27:54Z","author_association":"MEMBER","body":"Minimized (no need to run in incremental mode):\r\n\r\n```\r\n(set-logic QF_ANIA)\r\n(declare-fun x () Int)\r\n(declare-fun a () (Array Int (Array Int Int)))\r\n(declare-fun b () (Array Int (Array Int Int)))\r\n(declare-fun c () (Array Int (Array Int Int)))\r\n(assert (and (= (store a x (store (select a x) 0 0)) c) (= (store (store c 0 (store (select c 0) 0 0)) 0 (store (select (store c 0 (store (select c 0) 0 0)) 0) 0 (select (select b 0) 0))) b) (not (= 0 x))))\r\n(check-sat)\r\n```"}}
{"actor":{"display_login":"4tXJ7f"}}