{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/109","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/109/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/109/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/109/events","html_url":"https://github.com/Z3Prover/z3/issues/109","id":80970403,"number":109,"title":"iZ3 - Interpolator crashes","user":{"login":"MarcusVoelker","id":717556,"avatar_url":"https://avatars.githubusercontent.com/u/717556?v=3","gravatar_id":"","url":"https://api.github.com/users/MarcusVoelker","html_url":"https://github.com/MarcusVoelker","followers_url":"https://api.github.com/users/MarcusVoelker/followers","following_url":"https://api.github.com/users/MarcusVoelker/following{/other_user}","gists_url":"https://api.github.com/users/MarcusVoelker/gists{/gist_id}","starred_url":"https://api.github.com/users/MarcusVoelker/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/MarcusVoelker/subscriptions","organizations_url":"https://api.github.com/users/MarcusVoelker/orgs","repos_url":"https://api.github.com/users/MarcusVoelker/repos","events_url":"https://api.github.com/users/MarcusVoelker/events{/privacy}","received_events_url":"https://api.github.com/users/MarcusVoelker/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":{"login":"kenmcmil","id":8010069,"avatar_url":"https://avatars.githubusercontent.com/u/8010069?v=3","gravatar_id":"","url":"https://api.github.com/users/kenmcmil","html_url":"https://github.com/kenmcmil","followers_url":"https://api.github.com/users/kenmcmil/followers","following_url":"https://api.github.com/users/kenmcmil/following{/other_user}","gists_url":"https://api.github.com/users/kenmcmil/gists{/gist_id}","starred_url":"https://api.github.com/users/kenmcmil/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kenmcmil/subscriptions","organizations_url":"https://api.github.com/users/kenmcmil/orgs","repos_url":"https://api.github.com/users/kenmcmil/repos","events_url":"https://api.github.com/users/kenmcmil/events{/privacy}","received_events_url":"https://api.github.com/users/kenmcmil/received_events","type":"User","site_admin":false},"milestone":null,"comments":3,"created_at":"2015-05-26T13:50:26Z","updated_at":"2015-05-27T11:25:42Z","closed_at":"2015-05-27T10:24:16Z","body":"I found a test case where the ComputeInterpolant function crashes, probably with a segfault:\r\n```\r\n# A fatal error has been detected by the Java Runtime Environment:\r\n#\r\n#  EXCEPTION_UNCAUGHT_CXX_EXCEPTION (0xe06d7363) at pc=0x00007ff9daec8b9c, pid=8644, tid=7860\r\n```\r\n\r\nHere is some Java code to reproduce it:\r\n\r\n```java\r\nprivate void test() {\r\n    HashMap<String, String> options = new HashMap<>();\r\n    options.put(\"proof\", \"true\");\r\n    options.put(\"model\", \"true\");\r\n    InterpolationContext ctx = new InterpolationContext(options);\r\n    BoolExpr a = ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkBoolConst(\"#Init\"), ctx.mkBoolConst(\"#P0\")), ctx.mkNot(ctx.mkBoolConst(\"#IP_2\"))), ctx.mkEq(ctx.mkBoolConst(\"#IP_2\"), ctx.mkOr(ctx.mkNot(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr\"), ctx.mkInt(0))), ctx.mkAnd(ctx.mkNot(ctx.mkLe(ctx.mkDiv(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter\"), ctx.mkInt(16)), ctx.mkInt(-1))), ctx.mkOr(ctx.mkAnd(ctx.mkLe(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter\"), ctx.mkInt(1)), ctx.mkOr(ctx.mkLe(ctx.mkIntConst(\"#PC\"), ctx.mkInt(1)), ctx.mkNot(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr\"), ctx.mkInt(0)))), ctx.mkOr(ctx.mkGe(ctx.mkIntConst(\"#PC\"), ctx.mkInt(1)), ctx.mkNot(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr\"), ctx.mkInt(0))))), ctx.mkNot(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr\"), ctx.mkInt(0)))))))), ctx.mkEq(ctx.mkBoolConst(\"#Init\"), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter\"), ctx.mkInt(0)), ctx.mkEq(ctx.mkIntConst(\"#PC\"), ctx.mkInt(0))))), ctx.mkEq(ctx.mkBoolConst(\"#P0\"), ctx.mkLt(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter\"), ctx.mkInt(4)))), ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr\"), ctx.mkInt(0))), ctx.mkImplies(ctx.mkEq(ctx.mkIntConst(\"#PC\"), ctx.mkInt(0)), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'\"), ctx.mkITE(ctx.mkGe(ctx.mkMod((IntExpr) ctx.mkAdd(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter\"), ctx.mkInt(1)), ctx.mkInt(65536)), ctx.mkInt(32768)), ctx.mkSub(ctx.mkInt(65536), ctx.mkMod((IntExpr) ctx.mkAdd(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter\"), ctx.mkInt(1)), ctx.mkInt(65536))), ctx.mkMod((IntExpr) ctx.mkAdd(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter\"), ctx.mkInt(1)), ctx.mkInt(65536)))), ctx.mkEq(ctx.mkIntConst(\"#PC'\"), ctx.mkAdd(ctx.mkIntConst(\"#PC\"), ctx.mkInt(1))), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr\")))))), ctx.mkImplies(ctx.mkEq(ctx.mkIntConst(\"#PC\"), ctx.mkInt(1)), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'\"), ctx.mkMod(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter\"), ctx.mkInt(16))), ctx.mkEq(ctx.mkIntConst(\"#PC'\"), ctx.mkAdd(ctx.mkIntConst(\"#PC\"), ctx.mkInt(1))), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr\")))))), ctx.mkImplies(ctx.mkEq(ctx.mkIntConst(\"#PC\"), ctx.mkInt(2)), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"#PC'\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr\")), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr\")), ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'\"), ctx.mkIntConst(\"LOOP_SIXTEEN.Counter\")))))), ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'\"), ctx.mkInt(0))), ctx.mkImplies(ctx.mkEq(ctx.mkIntConst(\"#PC'\"), ctx.mkInt(0)), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter''\"), ctx.mkITE(ctx.mkGe(ctx.mkMod((IntExpr) ctx.mkAdd(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'\"), ctx.mkInt(1)), ctx.mkInt(65536)), ctx.mkInt(32768)), ctx.mkSub(ctx.mkInt(65536), ctx.mkMod((IntExpr) ctx.mkAdd(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'\"), ctx.mkInt(1)), ctx.mkInt(65536))), ctx.mkMod((IntExpr) ctx.mkAdd(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'\"), ctx.mkInt(1)), ctx.mkInt(65536)))), ctx.mkEq(ctx.mkIntConst(\"#PC''\"), ctx.mkAdd(ctx.mkIntConst(\"#PC'\"), ctx.mkInt(1))), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'\")))))), ctx.mkImplies(ctx.mkEq(ctx.mkIntConst(\"#PC'\"), ctx.mkInt(1)), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter''\"), ctx.mkMod(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'\"), ctx.mkInt(16))), ctx.mkEq(ctx.mkIntConst(\"#PC''\"), ctx.mkAdd(ctx.mkIntConst(\"#PC'\"), ctx.mkInt(1))), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'\")))))), ctx.mkImplies(ctx.mkEq(ctx.mkIntConst(\"#PC'\"), ctx.mkInt(2)), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"#PC''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'\")), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'\")), ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'\"))))));\r\n    BoolExpr b = ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr''\"), ctx.mkInt(0)), ctx.mkImplies(ctx.mkEq(ctx.mkIntConst(\"#PC''\"), ctx.mkInt(0)), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'''\"), ctx.mkITE(ctx.mkGe(ctx.mkMod((IntExpr) ctx.mkAdd(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter''\"), ctx.mkInt(1)), ctx.mkInt(65536)), ctx.mkInt(32768)), ctx.mkSub(ctx.mkInt(65536), ctx.mkMod((IntExpr) ctx.mkAdd(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter''\"), ctx.mkInt(1)), ctx.mkInt(65536))), ctx.mkMod((IntExpr) ctx.mkAdd(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter''\"), ctx.mkInt(1)), ctx.mkInt(65536)))), ctx.mkEq(ctx.mkIntConst(\"#PC'''\"), ctx.mkAdd(ctx.mkIntConst(\"#PC''\"), ctx.mkInt(1))), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr''\")))))), ctx.mkImplies(ctx.mkEq(ctx.mkIntConst(\"#PC''\"), ctx.mkInt(1)), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'''\"), ctx.mkMod(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter''\"), ctx.mkInt(16))), ctx.mkEq(ctx.mkIntConst(\"#PC'''\"), ctx.mkAdd(ctx.mkIntConst(\"#PC''\"), ctx.mkInt(1))), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr''\")))))), ctx.mkImplies(ctx.mkEq(ctx.mkIntConst(\"#PC''\"), ctx.mkInt(2)), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"#PC'''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr''\")), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.#adr''\")), ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'''\"), ctx.mkIntConst(\"LOOP_SIXTEEN.Counter''\")))))), ctx.mkEq(ctx.mkBoolConst(\"#IP_2'''\"), ctx.mkOr(ctx.mkNot(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'''\"), ctx.mkInt(0))), ctx.mkAnd(ctx.mkNot(ctx.mkLe(ctx.mkDiv(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'''\"), ctx.mkInt(16)), ctx.mkInt(-1))), ctx.mkOr(ctx.mkAnd(ctx.mkLe(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'''\"), ctx.mkInt(1)), ctx.mkOr(ctx.mkLe(ctx.mkIntConst(\"#PC'''\"), ctx.mkInt(1)), ctx.mkNot(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'''\"), ctx.mkInt(0)))), ctx.mkOr(ctx.mkGe(ctx.mkIntConst(\"#PC'''\"), ctx.mkInt(1)), ctx.mkNot(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'''\"), ctx.mkInt(0))))), ctx.mkNot(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.#adr'''\"), ctx.mkInt(0)))))))), ctx.mkEq(ctx.mkBoolConst(\"#Init'''\"), ctx.mkAnd(ctx.mkEq(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'''\"), ctx.mkInt(0)), ctx.mkEq(ctx.mkIntConst(\"#PC'''\"), ctx.mkInt(0))))), ctx.mkEq(ctx.mkBoolConst(\"#P0'''\"), ctx.mkLt(ctx.mkIntConst(\"LOOP_SIXTEEN.Counter'''\"), ctx.mkInt(4)))), ctx.mkAnd(ctx.mkNot(ctx.mkBoolConst(\"#Init'''\")), ctx.mkNot(ctx.mkBoolConst(\"#P0'''\"))));\r\n    BoolExpr pat = ctx.mkAnd(ctx.MkInterpolant(a), b);\r\n    ctx.ComputeInterpolant(pat, ctx.mkParams());\r\n    System.out.println(\"Everything okay\");\r\n}\r\n```\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/105876046","html_url":"https://github.com/Z3Prover/z3/issues/109#issuecomment-105876046","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/109","id":105876046,"user":{"login":"MarcusVoelker","id":717556,"avatar_url":"https://avatars.githubusercontent.com/u/717556?v=3","gravatar_id":"","url":"https://api.github.com/users/MarcusVoelker","html_url":"https://github.com/MarcusVoelker","followers_url":"https://api.github.com/users/MarcusVoelker/followers","following_url":"https://api.github.com/users/MarcusVoelker/following{/other_user}","gists_url":"https://api.github.com/users/MarcusVoelker/gists{/gist_id}","starred_url":"https://api.github.com/users/MarcusVoelker/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/MarcusVoelker/subscriptions","organizations_url":"https://api.github.com/users/MarcusVoelker/orgs","repos_url":"https://api.github.com/users/MarcusVoelker/repos","events_url":"https://api.github.com/users/MarcusVoelker/events{/privacy}","received_events_url":"https://api.github.com/users/MarcusVoelker/received_events","type":"User","site_admin":false},"created_at":"2015-05-27T11:25:42Z","updated_at":"2015-05-27T11:25:42Z","body":"The system I'm seeing this on is Windows, unstable, JDK 1.8.0. I can't tell the exact JDK version because I'm not at that system right now. I built the current HEAD of unstable yesterday, when I submitted the bug, so I would say it's not fixed yet. I'll see if I can dig up more information about this bug."}}