Multiple Segmentation Faults When Producing Proofs with "sat.euf=true tactic.default_tactic=smt..."

[SunHao-0]

Hi,

I played with z3 proof mode and tried the benchmark from this repo [1] (SMT-COMP data from many years). All the formulas under QF_BV/unsat were considered. It turned out that segment fault can be very easily triggered with those formulas (most are from real-world cases).

The uploaded file segv_cases.txt contains 137 file names that trigger SEGV, using the latest z3 built with the following command can reproduce:

for f in `cat segv_cases.txt`
do
# or tactic.default_tactic=sat
z3  sat.euf=true tactic.default_tactic=smt solver.proof.log=z3.proof.smt2 $f
done

segv_cases.txt

Note that when invoking z3 without solver.proof.log=z3.proof.smt2, SEGVs did not appear, and thus they were most likely due to the proof generation.

Some backtrace information from gdb about one of those crashes may help:

(gdb) r
Starting program: build/z3 sat.euf=true tactic.default_tactic=smt solver.proof.log=test.proof semantic-fusion-seeds/QF_BV/unsat/bench_707.smt2
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Program received signal SIGSEGV, Segmentation fault.
0x0000555555d75b15 in euf::solver::log_justifications(sat::literal, unsigned int, bool) ()
(gdb) bt
#0  0x0000555555d75b15 in euf::solver::log_justifications(sat::literal, unsigned int, bool) ()
#1  0x0000555555d3129c in euf::solver::get_antecedents(sat::literal, unsigned long, svector<sat::literal, unsigned int>&, bool) ()
#2  0x0000555556983a6b in sat::solver::process_consequent_for_unsat_core(sat::literal, sat::justification const&)
    ()
#3  0x0000555556983c7b in sat::solver::resolve_conflict_for_unsat_core() ()
#4  0x00005555569841f2 in sat::solver::drat_explain_conflict() ()
#5  0x000055555699411f in sat::solver::resolve_conflict_core() ()
#6  0x0000555556994949 in sat::solver::check_inconsistent() [clone .part.0] ()
#7  0x0000555556994d58 in sat::solver::check(unsigned int, sat::literal const*) ()
#8  0x0000555555cf474e in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#9  0x0000555555cf5ac8 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#10 0x00005555564a6592 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#11 0x00005555564c04ed in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ()
#12 0x00005555564c0d0e in 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> >&) ()
#13 0x0000555556416a16 in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) ()
#14 0x0000555556409821 in solver_na2as::check_sat_core(unsigned int, expr* const*) ()
#15 0x0000555556433e86 in combined_solver::check_sat_core(unsigned int, expr* const*) ()
#16 0x0000555556430f74 in solver::check_sat(unsigned int, expr* const*) ()
#17 0x00005555563d457f in cmd_context::check_sat(unsigned int, expr* const*) ()
#18 0x00005555563be3a2 in smt2::parser::operator()() ()
#19 0x00005555563a54c6 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*)
    ()
#20 0x00005555557a6b60 in read_smtlib2_commands(char const*) ()
#21 0x0000555555782b01 in main ()

These SEGVs are likely from very few root causes in the proof generation (new format, legacy mode seems stable). I am not an expert in this field, so posting here so that anyone interested can take a look.

Update: using z3 sat.smt=true solver.proof.log=... as mentioned in this issue does not trigger any SEGVs, since it does not produce any proof, which is a bit surprising to me.

[NikolajBjorner]

fixed

[SunHao-0]

Thanks! Also validated on my side, all the cases nicely handled.