{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/402","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/402/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/402/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/402/events","html_url":"https://github.com/Z3Prover/z3/issues/402","id":125155894,"number":402,"title":"Using quantifier body","user":{"login":"cheshire","id":348959,"avatar_url":"https://avatars.githubusercontent.com/u/348959?v=3","gravatar_id":"","url":"https://api.github.com/users/cheshire","html_url":"https://github.com/cheshire","followers_url":"https://api.github.com/users/cheshire/followers","following_url":"https://api.github.com/users/cheshire/following{/other_user}","gists_url":"https://api.github.com/users/cheshire/gists{/gist_id}","starred_url":"https://api.github.com/users/cheshire/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cheshire/subscriptions","organizations_url":"https://api.github.com/users/cheshire/orgs","repos_url":"https://api.github.com/users/cheshire/repos","events_url":"https://api.github.com/users/cheshire/events{/privacy}","received_events_url":"https://api.github.com/users/cheshire/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/Z3Prover/z3/labels/bug","name":"bug","color":"fc2929"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2016-01-06T11:01:43Z","updated_at":"2016-01-06T15:17:17Z","closed_at":null,"body":"Hi,\r\n\r\nAfter I have obtained a quantifier body using `get_quantifier_body`, can I do anything with it?\r\nE.g. replacing \"exists\" by \"forall\" or vice versa?\r\n\r\nI've tried giving the obtained body to `mk_forall` (while supplying no patterns or bound variables),\r\nand that dies with a segfault.\r\nWhat would be the proper way to do this?"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/169351926","html_url":"https://github.com/Z3Prover/z3/issues/402#issuecomment-169351926","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/402","id":169351926,"user":{"login":"wintersteiger","id":10155819,"avatar_url":"https://avatars.githubusercontent.com/u/10155819?v=3","gravatar_id":"","url":"https://api.github.com/users/wintersteiger","html_url":"https://github.com/wintersteiger","followers_url":"https://api.github.com/users/wintersteiger/followers","following_url":"https://api.github.com/users/wintersteiger/following{/other_user}","gists_url":"https://api.github.com/users/wintersteiger/gists{/gist_id}","starred_url":"https://api.github.com/users/wintersteiger/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wintersteiger/subscriptions","organizations_url":"https://api.github.com/users/wintersteiger/orgs","repos_url":"https://api.github.com/users/wintersteiger/repos","events_url":"https://api.github.com/users/wintersteiger/events{/privacy}","received_events_url":"https://api.github.com/users/wintersteiger/received_events","type":"User","site_admin":false},"created_at":"2016-01-06T15:17:17Z","updated_at":"2016-01-06T15:17:17Z","body":"Thanks for the quick test case, that helps a lot!\r\n\r\nThe actual problem here is not the creation of the quantifier, but the addition of formula to the solver while it still contains unbound variables. That can't be checked during construction, but should probably be checked somewhere within `s.add(constr2)` or `s.check()`."}}