{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/798","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/798/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/798/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/798/events","html_url":"https://github.com/Z3Prover/z3/issues/798","id":190614867,"number":798,"title":"A double free issue","user":{"login":"qingkaishi","id":6349384,"avatar_url":"https://avatars.githubusercontent.com/u/6349384?v=3","gravatar_id":"","url":"https://api.github.com/users/qingkaishi","html_url":"https://github.com/qingkaishi","followers_url":"https://api.github.com/users/qingkaishi/followers","following_url":"https://api.github.com/users/qingkaishi/following{/other_user}","gists_url":"https://api.github.com/users/qingkaishi/gists{/gist_id}","starred_url":"https://api.github.com/users/qingkaishi/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/qingkaishi/subscriptions","organizations_url":"https://api.github.com/users/qingkaishi/orgs","repos_url":"https://api.github.com/users/qingkaishi/repos","events_url":"https://api.github.com/users/qingkaishi/events{/privacy}","received_events_url":"https://api.github.com/users/qingkaishi/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":16,"created_at":"2016-11-21T04:17:21Z","updated_at":"2016-11-22T13:48:21Z","closed_at":null,"body":"I am using incremental z3 solver (4.5.0) in multithread context and find a double free crash. The stack backtrace is as following, can you help?\r\n\r\n```\r\n*** Error in a.out: double free or corruption (out): 0x00007f4d3618baf0 ***\r\n\r\n#0 0xbc3eb8 llvm::sys::PrintStackTrace(_IO_FILE*) (/home/qingkaishi/pinpoint/Release+Asserts/bin/pp-check+0xbc3eb8)\r\n#1 0xbc53ab SignalHandler(int) (/home/qingkaishi/pinpoint/Release+Asserts/bin/pp-check+0xbc53ab)\r\n#2 0x7f52fd5cd3e0 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x113e0)\r\n#3 0x7f52fb927428 gsignal /build/glibc-Qz8a69/glibc-2.23/signal/../sysdeps/unix/sysv/linux/raise.c:54:0\r\n#4 0x7f52fb92902a abort /build/glibc-Qz8a69/glibc-2.23/stdlib/abort.c:91:0\r\n#5 0x7f52fb9697ea /build/glibc-Qz8a69/glibc-2.23/libio/../sysdeps/posix/libc_fatal.c:175:0\r\n#6 0x7f52fb971e0a _int_free /build/glibc-Qz8a69/glibc-2.23/malloc/malloc.c:4103:0\r\n#7 0x7f52fb97598c cfree /build/glibc-Qz8a69/glibc-2.23/malloc/malloc.c:2967:0\r\n#8 0x7f52fcb917ce memory::deallocate(void*) (/usr/lib/libz3.so+0xed67ce)\r\n#9 0x7f52fcad7092 sat::clause_allocator::del_clause(sat::clause*) (/usr/lib/libz3.so+0xe1c092)\r\n#10 0x7f52fcabe533 sat::solver::~solver() (/usr/lib/libz3.so+0xe03533)\r\n#11 0x7f52fc752a3c sat_tactic::imp::~imp() (/usr/lib/libz3.so+0xa97a3c)\r\n#12 0x7f52fc752d55 sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (/usr/lib/libz3.so+0xa97d55)\r\n#13 0x7f52fc81eede cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (/usr/lib/libz3.so+0xb63ede)\r\n#14 0x7f52fc823bc5 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (/usr/lib/libz3.so+0xb68bc5)\r\n#15 0x7f52fc823bc5 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (/usr/lib/libz3.so+0xb68bc5)\r\n#16 0x7f52fc823bc5 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (/usr/lib/libz3.so+0xb68bc5)\r\n#17 0x7f52fc823bc5 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (/usr/lib/libz3.so+0xb68bc5)\r\n#18 0x7f52fc81a574 exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (/usr/lib/libz3.so+0xb5f574)\r\n#19 0x7f52fc81aa7d check_sat(tactic&, ref<goal>&, ref<model>&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) (/usr/lib/libz3.so+0xb5fa7d)\r\n#20 0x7f52fc672b1e tactic2solver::check_sat_core(unsigned int, expr* const*) (/usr/lib/libz3.so+0x9b7b1e)\r\n#21 0x7f52fc67802f solver_na2as::check_sat(unsigned int, expr* const*) (/usr/lib/libz3.so+0x9bd02f)\r\n#22 0x7f52fc67db14 combined_solver::check_sat(unsigned int, expr* const*) (/usr/lib/libz3.so+0x9c2b14)\r\n#23 0x7f52fbdafa1f Z3_solver_check (/usr/lib/libz3.so+0xf4a1f)\r\n```"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/262244572","html_url":"https://github.com/Z3Prover/z3/issues/798#issuecomment-262244572","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/798","id":262244572,"user":{"login":"qingkaishi","id":6349384,"avatar_url":"https://avatars.githubusercontent.com/u/6349384?v=3","gravatar_id":"","url":"https://api.github.com/users/qingkaishi","html_url":"https://github.com/qingkaishi","followers_url":"https://api.github.com/users/qingkaishi/followers","following_url":"https://api.github.com/users/qingkaishi/following{/other_user}","gists_url":"https://api.github.com/users/qingkaishi/gists{/gist_id}","starred_url":"https://api.github.com/users/qingkaishi/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/qingkaishi/subscriptions","organizations_url":"https://api.github.com/users/qingkaishi/orgs","repos_url":"https://api.github.com/users/qingkaishi/repos","events_url":"https://api.github.com/users/qingkaishi/events{/privacy}","received_events_url":"https://api.github.com/users/qingkaishi/received_events","type":"User","site_admin":false},"created_at":"2016-11-22T13:48:21Z","updated_at":"2016-11-22T13:48:21Z","body":"I mean, when my program starts, I can see log info are appended to the log file. However, after my program runs for a while, no more logs are appended to the log file, although I am sure the program are still doing z3 operations. Do you think this is an abnormal behavior? I can see this \"abnormal\" behavior when using z3-4.5.0 and the current master branch."}}
{"actor":{"display_login":"qingkaishi"}}