{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/98","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/98/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/98/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/98/events","html_url":"https://github.com/Z3Prover/z3/issues/98","id":78610969,"number":98,"title":"crash on malformed bv expression through API","user":{"login":"nunoplopes","id":2998477,"avatar_url":"https://avatars.githubusercontent.com/u/2998477?v=3","gravatar_id":"","url":"https://api.github.com/users/nunoplopes","html_url":"https://github.com/nunoplopes","followers_url":"https://api.github.com/users/nunoplopes/followers","following_url":"https://api.github.com/users/nunoplopes/following{/other_user}","gists_url":"https://api.github.com/users/nunoplopes/gists{/gist_id}","starred_url":"https://api.github.com/users/nunoplopes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nunoplopes/subscriptions","organizations_url":"https://api.github.com/users/nunoplopes/orgs","repos_url":"https://api.github.com/users/nunoplopes/repos","events_url":"https://api.github.com/users/nunoplopes/events{/privacy}","received_events_url":"https://api.github.com/users/nunoplopes/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"nunoplopes","id":2998477,"avatar_url":"https://avatars.githubusercontent.com/u/2998477?v=3","gravatar_id":"","url":"https://api.github.com/users/nunoplopes","html_url":"https://github.com/nunoplopes","followers_url":"https://api.github.com/users/nunoplopes/followers","following_url":"https://api.github.com/users/nunoplopes/following{/other_user}","gists_url":"https://api.github.com/users/nunoplopes/gists{/gist_id}","starred_url":"https://api.github.com/users/nunoplopes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nunoplopes/subscriptions","organizations_url":"https://api.github.com/users/nunoplopes/orgs","repos_url":"https://api.github.com/users/nunoplopes/repos","events_url":"https://api.github.com/users/nunoplopes/events{/privacy}","received_events_url":"https://api.github.com/users/nunoplopes/received_events","type":"User","site_admin":false},"milestone":null,"comments":1,"created_at":"2015-05-20T17:11:08Z","updated_at":"2015-05-26T08:31:35Z","closed_at":null,"body":"The following script crashes on Cygwin 32 (but not 64):\r\n```\r\nfrom z3 import *\r\nprint ZeroExt(2, ZeroExt(2, BitVecVal(0, 3))) - BitVecVal(0, 5)\r\n```\r\n\r\nstack trace:\r\n\r\n```\r\n#0  0x6c1229de in format_ns::mk_compose(ast_manager&, app*, app*, app*, app*)\r\n    () from libz3.dll\r\n#1  0x6c0ef068 in app* format_ns::mk_seq1<app**, format_ns::f2f>(ast_manager&, app** const&, app** const&, format_ns::f2f, char const*, char const*, char const*) [clone .constprop.201] () from libz3.dll\r\n#2  0x6c0ef28b in smt2_pp_environment::pp_sort(sort*) ()\r\n   from libz3.dll\r\n#3  0x6c0f11a9 in ast_smt2_pp(std::ostream&, sort*, smt2_pp_environment&, params_ref const&, unsigned int) () from libz3.dll\r\n#4  0x6c0f3845 in operator<<(std::ostream&, mk_ismt2_pp const&) ()\r\n   from libz3.dll\r\n#5  0x6c0d83b8 in ast_manager::check_sort(func_decl const*, unsigned int, expr* const*) const () from libz3.dll\r\n#6  0x6c0d86a6 in ast_manager::check_sorts_core(ast const*) const ()\r\n   from libz3.dll\r\n#7  0x6c0d8768 in ast_manager::check_sorts(ast const*) const ()\r\n   from libz3.dll\r\n#8  0x6bc75017 in api::context::check_sorts(ast*) ()\r\n   from libz3.dll\r\n#9  0x6bc60f68 in Z3_mk_bvsub () from libz3.dll\r\n```"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/105444747","html_url":"https://github.com/Z3Prover/z3/issues/98#issuecomment-105444747","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/98","id":105444747,"user":{"login":"nunoplopes","id":2998477,"avatar_url":"https://avatars.githubusercontent.com/u/2998477?v=3","gravatar_id":"","url":"https://api.github.com/users/nunoplopes","html_url":"https://github.com/nunoplopes","followers_url":"https://api.github.com/users/nunoplopes/followers","following_url":"https://api.github.com/users/nunoplopes/following{/other_user}","gists_url":"https://api.github.com/users/nunoplopes/gists{/gist_id}","starred_url":"https://api.github.com/users/nunoplopes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nunoplopes/subscriptions","organizations_url":"https://api.github.com/users/nunoplopes/orgs","repos_url":"https://api.github.com/users/nunoplopes/repos","events_url":"https://api.github.com/users/nunoplopes/events{/privacy}","received_events_url":"https://api.github.com/users/nunoplopes/received_events","type":"User","site_admin":false},"created_at":"2015-05-26T08:31:35Z","updated_at":"2015-05-26T08:31:35Z","body":"Update: this happens only with -O3, but not with -O2.\r\nGCC is assuming the stack is 16-byte aligned and issuing a 'movaps' instruction. Since memory is actually not aligned, we get a crash.  Investigating whether it's Z3's fault or a bug in GCC 4.9.."}}