par-or tactic triggers a segmentation fault

[daniel-larraz]

Consider this SMTLIB script: game.lus.contractck.4.txt

Most of the time z3 runs OK on the file, but sometimes z3 triggers a segmentation fault. Here is the backtrace I got with GDB:

[New LWP 15675]
[New LWP 15673]
Core was generated by `z3 game.lus.contractck.4.smt2'.
Program terminated with signal SIGSEGV, Segmentation fault.
#0  0x0000000001271a23 in model_evaluator::model_evaluator(model_core&, params_ref const&) ()
[Current thread is 1 (LWP 15675)]
(gdb) bt
#0  0x0000000001271a23 in model_evaluator::model_evaluator(model_core&, params_ref const&) ()
#1  0x00000000009c2bf6 in qe::quant_elim_plugin::check(unsigned int, app* const*, expr*, obj_ref<expr, ast_manager>&, bool, ref_vector<app, ast_manager>&, qe::guarded_defs*) ()
#2  0x00000000009c341b in qe::quant_elim_new::eliminate_block(unsigned int, app* const*, obj_ref<expr, ast_manager>&, ref_vector<app, ast_manager>&, bool, qe::guarded_defs*) ()
#3  0x00000000009b788c in qe::quant_elim_new::eliminate_exists_bind(unsigned int, app* const*, obj_ref<expr, ast_manager>&) ()
#4  0x00000000009b38d6 in qe::expr_quant_elim::elim(obj_ref<expr, ast_manager>&) ()
#5  0x00000000009b3a8d in qe::expr_quant_elim::operator()(expr*, expr*, obj_ref<expr, ast_manager>&) ()
#6  0x00000000009f9927 in qe_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#7  0x00000000009f9de6 in qe_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#8  0x000000000125264e in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#9  0x000000000125481d in std::thread::_State_impl<std::thread::_Invoker<std::tuple<par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}> > >::_M_run() ()
--Type <RET> for more, q to quit, c to continue without paging--
#10 0x00000000019e1273 in execute_native_thread_routine ()
#11 0x0000000001a4f7a7 in start_thread ()
#12 0x0000000001ace080 in clone3 ()

The issue seems to happen only when the par-or tactic is used. Using only either qe or qe2 instead of the par-or tactic works fine.

[daniel-larraz]

Backtrace with symbols:

[New LWP 28894]
[New LWP 28892]
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
Core was generated by `z3-dbg game.lus.contractck.4.smt2'.
Program terminated with signal SIGSEGV, Segmentation fault.
#0  0x000055ccebda66d8 in model_core::get_manager (this=0x0) at ../src/model/model_core.h:43
43          ast_manager & get_manager() const { return m; }
[Current thread is 1 (Thread 0x7f7122a57700 (LWP 28894))]
(gdb) 
(gdb) bt
#0  0x000055ccebda66d8 in model_core::get_manager (this=0x0) at ../src/model/model_core.h:43
#1  0x000055ccecef64ba in model_evaluator::imp::imp (this=0x7f711407fa30, md=..., p=...) at ../src/model/model_evaluator.cpp:681
#2  0x000055cceceecbfe in model_evaluator::model_evaluator (this=0x7f7114066680, md=..., p=...) at ../src/model/model_evaluator.cpp:692
#3  0x000055ccec17abb2 in qe::quant_elim_plugin::final_check (this=0x7f7114001c40) at ../src/qe/qe.cpp:1507
#4  0x000055ccec179fda in qe::quant_elim_plugin::check (this=0x7f7114001c40, num_vars=2, vars=0x7f7114000d78, assumption=0x55ccee54dda0, fml=..., 
    get_first=false, free_vars=..., defs=0x0) at ../src/qe/qe.cpp:1442
#5  0x000055ccec180d8f in qe::quant_elim_new::eliminate_block (this=0x55ccee554d10, num_vars=2, vars=0x7f7114000d78, fml=..., free_vars=..., get_first=false, 
    defs=0x0) at ../src/qe/qe.cpp:2145
#6  0x000055ccec180696 in qe::quant_elim_new::eliminate_exists (this=0x55ccee554d10, num_vars=2, vars=0x7f7114000d78, fml=..., free_vars=..., 
    get_first=false, defs=0x0) at ../src/qe/qe.cpp:2096
#7  0x000055ccec1817d0 in qe::quant_elim_new::eliminate_exists_bind (this=0x55ccee554d10, num_vars=2, vars=0x7f7114000d78, fml=...) at ../src/qe/qe.cpp:2189
#8  0x000055ccec180244 in qe::quant_elim_new::eliminate (this=0x55ccee554d10, is_forall=false, num_vars=2, vars=0x7f7114000d78, fml=...)
    at ../src/qe/qe.cpp:2060
--Type <RET> for more, q to quit, c to continue without paging--
#9  0x000055ccec16dab8 in qe::expr_quant_elim::elim (this=0x55ccee554c90, result=...) at ../src/qe/qe.cpp:2337
#10 0x000055ccec16cbf1 in qe::expr_quant_elim::operator() (this=0x55ccee554c90, assumption=0x55ccee54dda0, fml=0x55ccee554260, result=...)
    at ../src/qe/qe.cpp:2228
#11 0x000055ccec15a7c8 in qe_tactic::imp::operator() (this=0x55ccee554970, g=..., result=...) at ../src/qe/qe_tactic.cpp:65
#12 0x000055ccec15acf5 in qe_tactic::operator() (this=0x55ccee554930, in=..., result=...) at ../src/qe/qe_tactic.cpp:118
#13 0x000055ccece7538d in cleanup_tactical::operator() (this=0x55ccee554d60, in=..., result=...) at ../src/tactic/tactical.cpp:1032
#14 0x000055ccece71cd5 in par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda(unsigned int)#1}::operator()(unsigned int) const (
    __closure=0x7fff51844e40, i=1) at ../src/tactic/tactical.cpp:507
#15 0x000055ccece72170 in par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}::operator()() const (__closure=0x55ccee554f08)
    at ../src/tactic/tactical.cpp:554
#16 0x000055ccece79d2c in std::__invoke_impl<void, par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}>(std::__invoke_other, par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}&&) (__f=...) at /usr/include/c++/9/bits/invoke.h:60
#17 0x000055ccece79c7e in std::__invoke<par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}>(std::__invoke_result&&, (par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}&&)...) (__fn=...) at /usr/include/c++/9/bits/invoke.h:95
#18 0x000055ccece79bc0 in std::thread::_Invoker<std::tuple<par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}> >::_M_invoke<0ul>(std::_Index_tuple<0ul>) (this=0x55ccee554f08) at /usr/include/c++/9/thread:244
#19 0x000055ccece79b62 in std::thread::_Invoker<std::tuple<par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}> >::operator()() (
    this=0x55ccee554f08) at /usr/include/c++/9/thread:251
#20 0x000055ccece79b24 in std::thread::_State_impl<std::thread::_Invoker<std::tuple<par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}> > >::_M_run() (this=0x55ccee554f00) at /usr/include/c++/9/thread:195
#21 0x00007f7126756de4 in ?? () from /lib/x86_64-linux-gnu/libstdc++.so.6
#22 0x00007f712686a609 in start_thread (arg=<optimized out>) at pthread_create.c:477
#23 0x00007f7126443133 in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:95

Version: e423fab

[NikolajBjorner]

I can't repro it easily, but it has to be that one solver finished and canceled the other that just was retrieving a model. Then as it was canceled it returned the null model. I will later push a fix that checks for the null model to avoid the crash and you can see if it helps.

[daniel-larraz]

Sounds good. Thanks.

[daniel-larraz]

I tested the fix with the script above and more examples and the issue didn't show up again. The fix seems to work fine. Thanks!