failed to produce IUC #8
Comments
hgvk94
pushed a commit
that referenced
this issue
Aug 4, 2023
…junctions (Z3Prover#6779) After introducing the rewriter.sort_disjunctions option (Z3Prover#6774), I noticed a segfault in a Z3 run that was working fine for me before the PR. I traced the difference to a slight discrepancy between the first patch I submitted and the one we ended up merging: my first version would skip sorting the disjuncts in mk_nflat_core, but still return BR_DONE, while the patch in master returns BR_FAILED instead. This patch fixes that problem, and it makes slightly more sense to me to return a BR_DONE since, if `s` is true, some disjunct (e.g. a `false` or a repeat) might have been simplified away. However I don't fully understand this code. ... and I can't say I understand why the segfault happens. Perhaps that is a separate issue? This is the file to reproduce: https://gist.github.com/mtzguido/b7360c74d3d2e42d89f1bd9149ad26f6 Here's a stack trace of the failure, mk_nflat_or_core is not involved. ``` (gdb) where #0 0x0000555555b98497 in smt::context::get_lit_assignment(unsigned int) const () #1 0x0000555555b984cb in smt::context::get_assignment(sat::literal) const () #2 0x0000555555b98504 in smt::context::get_assignment(unsigned int) const () #3 0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const () #4 0x0000555555c9af5a in smt::context::get_assignment(expr*) const () #5 0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) () #6 0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) () #7 0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) () #8 0x0000555555c9c1b7 in smt::context::decide() () #9 0x0000555555ca39fd in smt::context::bounded_search() () #10 0x0000555555ca30c2 in smt::context::search() () Z3Prover#11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) () Z3Prover#12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) () Z3Prover#13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) () Z3Prover#14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) () Z3Prover#15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) () Z3Prover#16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) () Z3Prover#17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) () Z3Prover#18 0x0000555556082ff0 in smt2::parser::parse_check_sat() () Z3Prover#19 0x0000555556084dc0 in smt2::parser::parse_cmd() () Z3Prover#20 0x00005555560861b6 in smt2::parser::operator()() () Z3Prover#21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) () Z3Prover#22 0x00005555555e8f68 in read_smtlib2_commands(char const*) () Z3Prover#23 0x00005555555ee6f6 in main () (gdb) ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
cmd line args:
fp.engine=spacercommit: 92c15a3
benchmark: https://github.com/zafer-esen/tricera-adt-arr/blob/main/adt-arr/alternating_list-1.i.smt2
Looks like the proof is using an axiom that is assumed inside Spacer. I.e. this proof step is neither a theory hypothesis/axiom nor a part of TR/POB
The text was updated successfully, but these errors were encountered: