{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/243","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/243/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/243/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/243/events","html_url":"https://github.com/Z3Prover/z3/issues/243","id":111173239,"number":243,"title":"iZ3 - Segfaults","user":{"login":"stieglma","id":6758666,"avatar_url":"https://avatars.githubusercontent.com/u/6758666?v=3","gravatar_id":"","url":"https://api.github.com/users/stieglma","html_url":"https://github.com/stieglma","followers_url":"https://api.github.com/users/stieglma/followers","following_url":"https://api.github.com/users/stieglma/following{/other_user}","gists_url":"https://api.github.com/users/stieglma/gists{/gist_id}","starred_url":"https://api.github.com/users/stieglma/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/stieglma/subscriptions","organizations_url":"https://api.github.com/users/stieglma/orgs","repos_url":"https://api.github.com/users/stieglma/repos","events_url":"https://api.github.com/users/stieglma/events{/privacy}","received_events_url":"https://api.github.com/users/stieglma/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/Z3Prover/z3/labels/bug","name":"bug","color":"fc2929"}],"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":32,"created_at":"2015-10-13T12:50:21Z","updated_at":"2016-02-23T20:26:08Z","closed_at":"2016-02-23T20:26:08Z","body":"Hi,\r\n\r\nThis is the successor #64. We have still segfaults that occur when using Z3 for interpolation. Here are \r\nsome logs (replaying them results in errors caused by ```invalid pointer```). \r\n\r\nhttp://students.fim.uni-passau.de/~stieglma/z3/z3_log_elevator_spec13_product23_true-unreach-call.log.gz\r\nhttp://students.fim.uni-passau.de/~stieglma/z3/z3_log_problem14_label50.log.gz\r\nhttp://students.fim.uni-passau.de/~stieglma/z3/z3_log_s3_srvr_8_true-unreach-call.log.gz\r\n\r\nThese logs were produced with CPAchecker in Revision 18008 and Z3, unstable-branch, revision 7b95d6894abcc09c9f3ccb70deae13bace2864f0\r\n\r\nWe are quite sure that these segfaults are not caused by wrong/too much dec_refs. To prove this I temporarily commented out all dec_refs and did an inc_ref on each returned value of a Z3 function call where possible, the results stayed the same.\r\n\r\nIf you need further information, do not hesitate to contact me."},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/187888138","html_url":"https://github.com/Z3Prover/z3/issues/243#issuecomment-187888138","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/243","id":187888138,"user":{"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},"created_at":"2016-02-23T20:26:08Z","updated_at":"2016-02-23T20:26:08Z","body":"I can see that it's a pretty serious problem if you're running iZ3 under java. Unfortunately, the method iz3translate_main that's causing the problem has a pretty complicated recursion pattern with about a dozen recursive calls. If you tried to refactor this into an iterative routine, you'd almost certainly introduce subtle bugs (subtle because some of the cases occur rarely and are very difficult to stimulate). I'm going to mark this issue closed, as I think it's impractical to fix."}}