{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/219","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/219/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/219/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/219/events","html_url":"https://github.com/Z3Prover/z3/issues/219","id":106203541,"number":219,"title":"iz3 Z3_get_interpolant bad access","user":{"login":"cgcgbcbc","id":3320660,"avatar_url":"https://avatars.githubusercontent.com/u/3320660?v=3","gravatar_id":"","url":"https://api.github.com/users/cgcgbcbc","html_url":"https://github.com/cgcgbcbc","followers_url":"https://api.github.com/users/cgcgbcbc/followers","following_url":"https://api.github.com/users/cgcgbcbc/following{/other_user}","gists_url":"https://api.github.com/users/cgcgbcbc/gists{/gist_id}","starred_url":"https://api.github.com/users/cgcgbcbc/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cgcgbcbc/subscriptions","organizations_url":"https://api.github.com/users/cgcgbcbc/orgs","repos_url":"https://api.github.com/users/cgcgbcbc/repos","events_url":"https://api.github.com/users/cgcgbcbc/events{/privacy}","received_events_url":"https://api.github.com/users/cgcgbcbc/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-09-13T07:50:03Z","updated_at":"2015-09-13T14:57:32Z","closed_at":"2015-09-13T09:24:27Z","body":"```cpp\r\n#include <iostream>\r\n#include <z3++.h>\r\n#include <z3.h>\r\n#include <z3_interp.h>\r\n\r\nint main() {\r\n    z3::config cfg;\r\n    cfg.set(\"PROOF\", true);\r\n    cfg.set(\"MODEL\", true);\r\n    z3::context ctx(cfg);\r\n    auto a = ctx.int_const(\"c\");\r\n    auto b = ctx.int_const(\"b\");\r\n    auto c = ctx.int_const(\"c\");\r\n    auto d = ctx.int_const(\"d\");\r\n    auto A = (a == b) && (a == c);\r\n    auto B = (b == d) && (! (c==d) );\r\n    auto A_ = Z3_mk_interpolant(ctx, A);\r\n    auto param2 = ctx.bool_val(false);\r\n    auto param3 = A_ && B;\r\n    auto param4 = Z3_mk_params(ctx);\r\n    Z3_get_interpolant(ctx, param2, param3, param4);\r\n    return 0;\r\n}\r\n```\r\nRunning result:\r\n```\r\nSegmentation fault: 11\r\n```\r\nDebug info:\r\n```\r\n* thread #1: tid = 0x3b67b, 0x0000000100468ded libz3.dylib`iz3mgr::arg(ast_r const&, int) + 45, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x380000014)\r\n    frame #0: 0x0000000100468ded libz3.dylib`iz3mgr::arg(ast_r const&, int) + 45\r\nlibz3.dylib`iz3mgr::arg:\r\n->  0x100468ded <+45>: incl   0x8(%rax)\r\n    0x100468df0 <+48>: movq   %rdi, %rax\r\n    0x100468df3 <+51>: popq   %rdx\r\n    0x100468df4 <+52>: retq   \r\n```\r\n\r\nz3 version: 4.4.0\r\nsystem version: OSX 10.11"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/139884996","html_url":"https://github.com/Z3Prover/z3/issues/219#issuecomment-139884996","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/219","id":139884996,"user":{"login":"cgcgbcbc","id":3320660,"avatar_url":"https://avatars.githubusercontent.com/u/3320660?v=3","gravatar_id":"","url":"https://api.github.com/users/cgcgbcbc","html_url":"https://github.com/cgcgbcbc","followers_url":"https://api.github.com/users/cgcgbcbc/followers","following_url":"https://api.github.com/users/cgcgbcbc/following{/other_user}","gists_url":"https://api.github.com/users/cgcgbcbc/gists{/gist_id}","starred_url":"https://api.github.com/users/cgcgbcbc/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cgcgbcbc/subscriptions","organizations_url":"https://api.github.com/users/cgcgbcbc/orgs","repos_url":"https://api.github.com/users/cgcgbcbc/repos","events_url":"https://api.github.com/users/cgcgbcbc/events{/privacy}","received_events_url":"https://api.github.com/users/cgcgbcbc/received_events","type":"User","site_admin":false},"created_at":"2015-09-13T14:57:32Z","updated_at":"2015-09-13T14:57:32Z","body":"finally get a working example by Z3_compute_interpolant ( which I found is used by python api)\r\n```cpp\r\n#include <iostream>\r\n#include <z3++.h>\r\n#include <z3.h>\r\n#include <z3_interp.h>\r\n\r\nint main() {\r\n    z3::config cfg;\r\n    cfg.set(\"PROOF\", true);\r\n    cfg.set(\"MODEL\", true);\r\n    z3::context ctx(cfg);\r\n    auto a = ctx.int_const(\"a\");\r\n    auto b = ctx.int_const(\"b\");\r\n    auto c = ctx.int_const(\"c\");\r\n    auto d = ctx.int_const(\"d\");\r\n    auto A = (a == b) && (a == c);\r\n    auto B = (b == d) && (! (c==d) );\r\n    auto A_ = z3::expr(ctx, Z3_mk_interpolant(ctx, A));\r\n    auto param2 = ctx.bool_val(false);\r\n    auto param3 = z3::expr(ctx, A_ && B);\r\n    z3::params param4(ctx);\r\n    //Z3_get_interpolant(ctx, param2, param3, param4);\r\n    Z3_ast_vector * vector = new Z3_ast_vector();\r\n    Z3_model * model = new Z3_model();\r\n    auto result = Z3_compute_interpolant(ctx, A_ && B, param4, vector, model);\r\n    if (result == Z3_L_TRUE) {\r\n        std::cout << \"true\" << std::endl;\r\n    } else if (result == Z3_L_FALSE) {\r\n        std::cout << \"false\" << std::endl;\r\n        std::cout << z3::ast_vector(ctx, *vector);\r\n    } else {\r\n        std::cout << \"unknown\" << std::endl;\r\n    }\r\n    return 0;\r\n}\r\n```"}}