From 7c380fd6a0e667cbeafb6ea88eec6cf1a09c5925 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 23 Jun 2023 11:45:29 -0700 Subject: [PATCH] bool_rewriter: fix possible segfault when disabling rewriter.sort_disjunctions (#6779) After introducing the rewriter.sort_disjunctions option (#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&, 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() () #11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) () #12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) () #13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) () #14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) () #15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) () #16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) () #17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) () #18 0x0000555556082ff0 in smt2::parser::parse_check_sat() () #19 0x0000555556084dc0 in smt2::parser::parse_cmd() () #20 0x00005555560861b6 in smt2::parser::operator()() () #21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream >&, bool, params_ref const&, char const*) () #22 0x00005555555e8f68 in read_smtlib2_commands(char const*) () #23 0x00005555555ee6f6 in main () (gdb) ``` --- src/ast/rewriter/bool_rewriter.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 16ecf6473..9806424a3 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -184,7 +184,7 @@ br_status bool_rewriter::mk_flat_and_core(unsigned num_args, expr * const * args } br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args, expr_ref & result) { - bool s = false; + bool s = false; // whether we have canceled some disjuncts or found some out or order ptr_buffer buffer; expr_fast_mark1 neg_lits; expr_fast_mark2 pos_lits; @@ -292,9 +292,11 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args if (st != BR_FAILED) return st; #endif - if (m_sort_disjunctions && s) { - ast_lt lt; - std::sort(buffer.begin(), buffer.end(), lt); + if (s) { + if (m_sort_disjunctions) { + ast_lt lt; + std::sort(buffer.begin(), buffer.end(), lt); + } result = m().mk_or(sz, buffer.data()); return BR_DONE; }