Created attachment 1935543 [details] Reproducer py-z3 script Description of problem: segfault while printing result after finding solution Version-Release number of selected component (if applicable): python3-z3.noarch 4.8.17-1.fc36 @updates z3.x86_64 4.8.17-1.fc36 @updates z3-libs.x86_64 4.8.17-1.fc36 @updates How reproducible: 100% (with set seed) Steps to Reproduce: 1. run attached (autogenerated) script Actual results: segfault at 562e47007f60 ip 00007f4b8a317153 sp 00007fffa3388950 error 4 in libz3.so.4.8.17.0[7f4b89c7c000+c80000] Code: f8 1c 00 00 83 43 34 01 48 85 d2 74 0a 8b 42 fc 83 e8 01 48 c1 e0 03 4c 8b 24 02 48 8b 83 40 1d 00 00 41 8b 14 24 48 8d 04 d0 <48> 8b 28 48 c7 00 00 00 00 00 48 3b 6d 18 0f b6 45 2c 0f 84 a5 00 Expected results: not segfault Additional info: $ objdump -dr /usr/lib64/libz3.so.4.8.17.0 | grep -e '153:' | grep '48 8b 28' 717153: 48 8b 28 mov rbp,QWORD PTR [rax] 717114: 48 b8 f8 ff ff ff 07 movabs rax,0x7fffffff8 71711b: 00 00 00 71711e: 41 54 push r12 717120: 55 push rbp 717121: 53 push rbx 717122: 48 8b 5f 08 mov rbx,QWORD PTR [rdi+0x8] 717126: 48 8b 93 f8 1c 00 00 mov rdx,QWORD PTR [rbx+0x1cf8] 71712d: 83 43 34 01 add DWORD PTR [rbx+0x34],0x1 717131: 48 85 d2 test rdx,rdx 717134: 74 0a je 717140 <std::ostream& std::ostream::_M_insert<long long>(long long)@plt+0x699540> 717136: 8b 42 fc mov eax,DWORD PTR [rdx-0x4] 717139: 83 e8 01 sub eax,0x1 71713c: 48 c1 e0 03 shl rax,0x3 717140: 4c 8b 24 02 mov r12,QWORD PTR [rdx+rax*1] 717144: 48 8b 83 40 1d 00 00 mov rax,QWORD PTR [rbx+0x1d40] 71714b: 41 8b 14 24 mov edx,DWORD PTR [r12] 71714f: 48 8d 04 d0 lea rax,[rax+rdx*8] 717153: *** 48 8b 28 ******* mov rbp,QWORD PTR [rax]
Thank you for the report, Alexey. I wonder why ABRT doesn't catch this crash. The segfault happens at src/smt/smt_internalizer.cpp, line 1064: enode * e = m_app2enode[n_id]; The instance variable m_app2enode contains a vector of size and capacity 3. The variable n_id holds the value 1454550984. I'll investigate.
> I wonder why ABRT doesn't catch this crash. I uninstalled it out of frustration, it used to get backtraces and then it stopped doing it for me for some reason :-( Anyhow, Attached script sometimes doesn't segfault if it finds different solution, I can probably find working seed if it helps. Also I have 2 very similar scripts with the same segfault signature.
Sorry, I meant that ABRT doesn't catch this crash for *me*. I get the segfault message on the terminal and ABRT ... does nothing whatsoever. It has caught other crashes, so I wonder why it doesn't catch this one. Here's what I know so far: - With GDB and a conditional breakpoint on the place where the IDs are generated, conditional on the ID being greater than 1000000, the breakpoint never fires. This suggests that the ID is changed after the object is created and added to m_e_internalized_stack. - With valgrind, the crash doesn't happen. The only warning is about use of an uninitialized value, which has nothing to do with the crash. (Verified by patching the code to initialize that value; the crash still happens.) - With -fsanitize=address added to the build flags, the crash doesn't happen, and we only get an error due to the same uninitialized value. With that patched, the script runs without crashing. - With -fsanitize=undefined added to the build flags, the crash doesn't happen and no undefined behavior is detected. - With a debug build of z3, rather than a release build, the crash doesn't happen, and the debug code doesn't see anything go wrong. (Debug builds use optimization level -O0.) - With the optimization level reduced from -O2 to -O1, the crash doesn't happen. I tried to do a build with -fsanitize=thread. Eight hours later, it is still trying to link. Furthermore, ld does not show up on the first page with either top or iotop, so I think it is wedged. If I can get a link to finish successfully, we can check on that.
I finally figured out the secret sauce to get a complete build with -fsanitize=thread. Sure enough, it shows some races. I suspect that the -O2 vs. -O1 result is a red herring; probably building with -O1 changed the performance characteristics of the code enough to make the crash less likely. The sanitizer report is below for the curious. Now I have to figure out what code changes will eliminate the races. ================== WARNING: ThreadSanitizer: data race (pid=75) Read of size 4 at 0x7b940176d880 by thread T2 (mutexes: write M1789): #0 ast::inc_ref() /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.h:485 (libz3.so.4.11+0x3c9b74) #1 ast_manager::inc_ref(ast*) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.h:1633 (libz3.so.4.11+0x3c9b74) #2 ast_translation::cache(ast*, ast*) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast_translation.cpp:52 (libz3.so.4.11+0x3c9b74) #3 ast_translation::mk_sort(sort*, ast_translation::frame&) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast_translation.cpp:139 (libz3.so.4.11+0x3d548d) #4 ast_translation::process(ast const*) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast_translation.cpp:315 (libz3.so.4.11+0x3d548d) #5 quantifier* ast_translation::translate<quantifier>(quantifier const*) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast_translation.h:80 (libz3.so.4.11+0x57cbb6) #6 expr* ast_translation::operator()<expr>(expr const*) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast_translation.h:73 (libz3.so.4.11+0x57cbb6) #7 model::translate(ast_translation&) const /builddir/build/BUILD/z3-z3-4.11.2/src/model/model.cpp:178 (libz3.so.4.11+0x57cbb6) #8 parallel_tactic::report_sat(parallel_tactic::solver_state&, solver*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:469 (libz3.so.4.11+0x819770) #9 parallel_tactic::cube_and_conquer(parallel_tactic::solver_state&) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:542 (libz3.so.4.11+0x81e005) #10 parallel_tactic::run_solver() /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:697 (libz3.so.4.11+0x81e005) #11 parallel_tactic::solve(ref<model>&)::{lambda()#1}::operator()() const /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:733 (libz3.so.4.11+0x81e005) #12 void std::__invoke_impl<void, parallel_tactic::solve(ref<model>&)::{lambda()#1}>(std::__invoke_other, parallel_tactic::solve(ref<model>&)::{lambda()#1}&&) /usr/include/c++/12/bits/invoke.h:61 (libz3.so.4.11+0x81e005) #13 std::__invoke_result<parallel_tactic::solve(ref<model>&)::{lambda()#1}>::type std::__invoke<parallel_tactic::solve(ref<model>&)::{lambda()#1}>(parallel_tactic::solve(ref<model>&)::{lambda()#1}&&) /usr/include/c++/12/bits/invoke.h:96 (libz3.so.4.11+0x81e005) #14 void std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> >::_M_invoke<0ul>(std::_Index_tuple<0ul>) /usr/include/c++/12/bits/std_thread.h:258 (libz3.so.4.11+0x81e005) #15 std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> >::operator()() /usr/include/c++/12/bits/std_thread.h:265 (libz3.so.4.11+0x81e005) #16 std::thread::_State_impl<std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> > >::_M_run() /usr/include/c++/12/bits/std_thread.h:210 (libz3.so.4.11+0x81e005) #17 execute_native_thread_routine <null> (libstdc++.so.6+0xdbc02) Previous write of size 4 at 0x7b940176d880 by thread T1: #0 ast::dec_ref() /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.h:490 (libz3.so.4.11+0x3aaee6) #1 ast_manager::dec_ref(ast*) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.h:1638 (libz3.so.4.11+0x3aaee6) #2 ref_manager_wrapper<expr, ast_manager>::dec_ref(expr*) /builddir/build/BUILD/z3-z3-4.11.2/src/util/ref_vector.h:227 (libz3.so.4.11+0x3aaee6) #3 ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_ref(expr*) /builddir/build/BUILD/z3-z3-4.11.2/src/util/ref_vector.h:37 (libz3.so.4.11+0x3aaee6) #4 ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_range_ref(expr* const*, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/util/ref_vector.h:41 (libz3.so.4.11+0x3aaee6) #5 ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::shrink(unsigned int) /builddir/build/BUILD/z3-z3-4.11.2/src/util/ref_vector.h:100 (libz3.so.4.11+0x3aaee6) #6 void rewriter_tpl<mev::evaluator_cfg>::process_app<false>(app*, rewriter_core::frame&) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/rewriter/rewriter_def.h:330 (libz3.so.4.11+0x59a07f) #7 void rewriter_tpl<mev::evaluator_cfg>::resume_core<false>(obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/rewriter/rewriter_def.h:787 (libz3.so.4.11+0x59a07f) #8 void rewriter_tpl<mev::evaluator_cfg>::main_loop<false>(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/rewriter/rewriter_def.h:746 (libz3.so.4.11+0x59a07f) #9 rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/rewriter/rewriter_def.h:826 (libz3.so.4.11+0x59a07f) #10 rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/rewriter/rewriter.h:360 (libz3.so.4.11+0x59a96f) #11 model_evaluator::operator()(expr*, obj_ref<expr, ast_manager>&) /builddir/build/BUILD/z3-z3-4.11.2/src/model/model_evaluator.cpp:744 (libz3.so.4.11+0x59a96f) #12 generic_model_converter::operator()(ref<model>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/generic_model_converter.cpp:59 (libz3.so.4.11+0x5bf585) #13 sat2goal::mc::operator()(ref<model>&) /builddir/build/BUILD/z3-z3-4.11.2/src/sat/tactic/sat2goal.cpp:144 (libz3.so.4.11+0x1254119) #14 inc_sat_solver::get_model_core(ref<model>&) /builddir/build/BUILD/z3-z3-4.11.2/src/sat/sat_solver/inc_sat_solver.cpp:1084 (libz3.so.4.11+0x1254119) #15 check_sat_result::get_model(ref<model>&) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/check_sat_result.h:59 (libz3.so.4.11+0x8049ff) #16 parallel_tactic::report_sat(parallel_tactic::solver_state&, solver*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:463 (libz3.so.4.11+0x819956) #17 parallel_tactic::cube_and_conquer(parallel_tactic::solver_state&) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:542 (libz3.so.4.11+0x81e005) #18 parallel_tactic::run_solver() /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:697 (libz3.so.4.11+0x81e005) #19 parallel_tactic::solve(ref<model>&)::{lambda()#1}::operator()() const /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:733 (libz3.so.4.11+0x81e005) #20 void std::__invoke_impl<void, parallel_tactic::solve(ref<model>&)::{lambda()#1}>(std::__invoke_other, parallel_tactic::solve(ref<model>&)::{lambda()#1}&&) /usr/include/c++/12/bits/invoke.h:61 (libz3.so.4.11+0x81e005) #21 std::__invoke_result<parallel_tactic::solve(ref<model>&)::{lambda()#1}>::type std::__invoke<parallel_tactic::solve(ref<model>&)::{lambda()#1}>(parallel_tactic::solve(ref<model>&)::{lambda()#1}&&) /usr/include/c++/12/bits/invoke.h:96 (libz3.so.4.11+0x81e005) #22 void std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> >::_M_invoke<0ul>(std::_Index_tuple<0ul>) /usr/include/c++/12/bits/std_thread.h:258 (libz3.so.4.11+0x81e005) #23 std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> >::operator()() /usr/include/c++/12/bits/std_thread.h:265 (libz3.so.4.11+0x81e005) #24 std::thread::_State_impl<std::thread::_Invoker<std::tuple<parallel_tactic::solve(ref<model>&)::{lambda()#1}> > >::_M_run() /usr/include/c++/12/bits/std_thread.h:210 (libz3.so.4.11+0x81e005) #25 execute_native_thread_routine <null> (libstdc++.so.6+0xdbc02) Location is heap block of size 8200 at 0x7b940176d800 allocated by main thread: #0 malloc <null> (libtsan.so.2.0.0+0x3f618) #1 memory::allocate(unsigned long) /builddir/build/BUILD/z3-z3-4.11.2/src/util/memory_manager.cpp:273 (libz3.so.4.11+0x1e36d6) #2 small_object_allocator::allocate(unsigned long) /builddir/build/BUILD/z3-z3-4.11.2/src/util/small_object_allocator.cpp:136 (libz3.so.4.11+0x213943) #3 ast_manager::allocate_node(unsigned int) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.h:1677 (libz3.so.4.11+0x361357) #4 ast_manager::mk_sort(symbol const&, sort_info*) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.cpp:1974 (libz3.so.4.11+0x361357) #5 ast_manager::mk_sort(symbol const&, sort_info const&) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.h:1706 (libz3.so.4.11+0x361357) #6 basic_decl_plugin::set_manager(ast_manager*, int) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.cpp:874 (libz3.so.4.11+0x38e043) #7 ast_manager::register_plugin(int, decl_plugin*) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.cpp:1691 (libz3.so.4.11+0x390f6f) #8 ast_manager::init() /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.cpp:1382 (libz3.so.4.11+0x3957c2) #9 ast_manager::ast_manager(proof_gen_mode, char const*, bool) /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.cpp:1327 (libz3.so.4.11+0x83bfd2) #10 ast_context_params::mk_ast_manager() /builddir/build/BUILD/z3-z3-4.11.2/src/cmd_context/cmd_context.cpp:317 (libz3.so.4.11+0x83bfd2) #11 api::context::context(ast_context_params*, bool) /builddir/build/BUILD/z3-z3-4.11.2/src/api/api_context.cpp:120 (libz3.so.4.11+0x1315706) #12 Z3_mk_context_rc /builddir/build/BUILD/z3-z3-4.11.2/src/api/api_context.cpp:384 (libz3.so.4.11+0x131698b) #13 ffi_call_unix64 <null> (libffi.so.8+0x7a05) Mutex M1789 (0x7b48000f66d0) created at: #0 pthread_mutex_lock <null> (libtsan.so.2.0.0+0x56341) #1 __gthread_mutex_lock /usr/include/c++/12/x86_64-redhat-linux/bits/gthr-default.h:749 (libz3.so.4.11+0x1e0cf0) #2 std::mutex::lock() /usr/include/c++/12/bits/std_mutex.h:100 (libz3.so.4.11+0x1e0cf0) #3 std::lock_guard<std::mutex>::lock_guard(std::mutex&) /usr/include/c++/12/bits/std_mutex.h:229 (libz3.so.4.11+0x81b575) #4 parallel_tactic::add_branches(unsigned int) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:426 (libz3.so.4.11+0x81b575) #5 parallel_tactic::solve(ref<model>&) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:730 (libz3.so.4.11+0x81b575) #6 parallel_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/parallel_tactic.cpp:801 (libz3.so.4.11+0x81b575) #7 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #8 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #9 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #10 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #11 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #12 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #13 unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:869 (libz3.so.4.11+0x5c83ee) #14 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #15 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #16 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #17 unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:869 (libz3.so.4.11+0x5c83ee) #18 exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactic.cpp:153 (libz3.so.4.11+0x5e7851) #19 check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, 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> >&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactic.cpp:173 (libz3.so.4.11+0x5e79fc) #20 check_sat_core2 /builddir/build/BUILD/z3-z3-4.11.2/src/solver/tactic2solver.cpp:229 (libz3.so.4.11+0x825dd6) #21 solver_na2as::check_sat_core(unsigned int, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/solver_na2as.cpp:67 (libz3.so.4.11+0x8245bf) #22 combined_solver::check_sat_core(unsigned int, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/combined_solver.cpp:252 (libz3.so.4.11+0x818fe1) #23 solver::check_sat(unsigned int, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/solver.cpp:318 (libz3.so.4.11+0x82fbad) #24 _solver_check /builddir/build/BUILD/z3-z3-4.11.2/src/api/api_solver.cpp:603 (libz3.so.4.11+0x137d254) #25 Z3_solver_check_assumptions /builddir/build/BUILD/z3-z3-4.11.2/src/api/api_solver.cpp:640 (libz3.so.4.11+0x137d660) #26 ffi_call_unix64 <null> (libffi.so.8+0x7a05) Thread T2 (tid=78, running) created by main thread at: #0 pthread_create <null> (libtsan.so.2.0.0+0x5f0e6) #1 std::thread::_M_start_thread(std::unique_ptr<std::thread::_State, std::default_delete<std::thread::_State> >, void (*)()) <null> (libstdc++.so.6+0xdbcd8) #2 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #3 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #4 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #5 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #6 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #7 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #8 unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:869 (libz3.so.4.11+0x5c83ee) #9 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #10 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #11 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #12 unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:869 (libz3.so.4.11+0x5c83ee) #13 exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactic.cpp:153 (libz3.so.4.11+0x5e7851) #14 check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, 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> >&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactic.cpp:173 (libz3.so.4.11+0x5e79fc) #15 check_sat_core2 /builddir/build/BUILD/z3-z3-4.11.2/src/solver/tactic2solver.cpp:229 (libz3.so.4.11+0x825dd6) #16 solver_na2as::check_sat_core(unsigned int, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/solver_na2as.cpp:67 (libz3.so.4.11+0x8245bf) #17 combined_solver::check_sat_core(unsigned int, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/combined_solver.cpp:252 (libz3.so.4.11+0x818fe1) #18 solver::check_sat(unsigned int, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/solver.cpp:318 (libz3.so.4.11+0x82fbad) #19 _solver_check /builddir/build/BUILD/z3-z3-4.11.2/src/api/api_solver.cpp:603 (libz3.so.4.11+0x137d254) #20 Z3_solver_check_assumptions /builddir/build/BUILD/z3-z3-4.11.2/src/api/api_solver.cpp:640 (libz3.so.4.11+0x137d660) #21 ffi_call_unix64 <null> (libffi.so.8+0x7a05) Thread T1 (tid=77, running) created by main thread at: #0 pthread_create <null> (libtsan.so.2.0.0+0x5f0e6) #1 std::thread::_M_start_thread(std::unique_ptr<std::thread::_State, std::default_delete<std::thread::_State> >, void (*)()) <null> (libstdc++.so.6+0xdbcd8) #2 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #3 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #4 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #5 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #6 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #7 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #8 unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:869 (libz3.so.4.11+0x5c83ee) #9 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #10 cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:1146 (libz3.so.4.11+0x5c89eb) #11 and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:121 (libz3.so.4.11+0x5d1a77) #12 unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactical.cpp:869 (libz3.so.4.11+0x5c83ee) #13 exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactic.cpp:153 (libz3.so.4.11+0x5e7851) #14 check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, 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> >&) /builddir/build/BUILD/z3-z3-4.11.2/src/tactic/tactic.cpp:173 (libz3.so.4.11+0x5e79fc) #15 check_sat_core2 /builddir/build/BUILD/z3-z3-4.11.2/src/solver/tactic2solver.cpp:229 (libz3.so.4.11+0x825dd6) #16 solver_na2as::check_sat_core(unsigned int, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/solver_na2as.cpp:67 (libz3.so.4.11+0x8245bf) #17 combined_solver::check_sat_core(unsigned int, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/combined_solver.cpp:252 (libz3.so.4.11+0x818fe1) #18 solver::check_sat(unsigned int, expr* const*) /builddir/build/BUILD/z3-z3-4.11.2/src/solver/solver.cpp:318 (libz3.so.4.11+0x82fbad) #19 _solver_check /builddir/build/BUILD/z3-z3-4.11.2/src/api/api_solver.cpp:603 (libz3.so.4.11+0x137d254) #20 Z3_solver_check_assumptions /builddir/build/BUILD/z3-z3-4.11.2/src/api/api_solver.cpp:640 (libz3.so.4.11+0x137d660) #21 ffi_call_unix64 <null> (libffi.so.8+0x7a05) SUMMARY: ThreadSanitizer: data race /builddir/build/BUILD/z3-z3-4.11.2/src/ast/ast.h:485 in ast::inc_ref() ================== 21588046043715261016963855891506337581457420190517045593279128147475457096817778437067338964686254364479332529801522494528451859937437465734041066114753891494058384776073915518451373243595767403494360932156710967426837763530846977895530787885295907044714521937915615666796096178328792667906587148560314082467953818920817828068558983417562665941335213518681936694151943480814374320519651720844575760060158544113994987244072729849819249779644167755043776685340705698395774188963118063 ThreadSanitizer: reported 1 warnings
Yes, it is parallelism. Disabling 'parallel.enable' produces solution reliably.
Thanks for the information, Alexey. I have a candidate patch to address the issue. I'm doing a build now and will run some tests as soon as it completes.
I just ran your segfault-147.py script half a dozen times in a row with no crash. I think we have a winner. I will start a Rawhide build right now. It is after my bedtime, so F36 and F37 builds, and submitting patches upstream, will happen tomorrow.
FEDORA-2023-a378a50154 has been submitted as an update to Fedora 37. https://bodhi.fedoraproject.org/updates/FEDORA-2023-a378a50154
FEDORA-2023-3143658cbc has been submitted as an update to Fedora 36. https://bodhi.fedoraproject.org/updates/FEDORA-2023-3143658cbc
Thank you so much. I'll test as soon as possible.
Upstream PR for the data race: https://github.com/Z3Prover/z3/pull/6528
FEDORA-2023-a378a50154 has been pushed to the Fedora 37 testing repository. Soon you'll be able to install the update with the following command: `sudo dnf upgrade --enablerepo=updates-testing --refresh --advisory=FEDORA-2023-a378a50154` You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2023-a378a50154 See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.
FEDORA-2023-3143658cbc has been pushed to the Fedora 36 testing repository. Soon you'll be able to install the update with the following command: `sudo dnf upgrade --enablerepo=updates-testing --refresh --advisory=FEDORA-2023-3143658cbc` You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2023-3143658cbc See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates.
Update fixes segfault here. Thanks again!
You're welcome.
FEDORA-2023-a378a50154 has been pushed to the Fedora 37 stable repository. If problem still persists, please make note of it in this bug report.
FEDORA-2023-3143658cbc has been pushed to the Fedora 36 stable repository. If problem still persists, please make note of it in this bug report.