bool_rewriter: fix possible segfault when disabling rewriter.sort_dis…

…junctions (#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<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() ()
 #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<char, std::char_traits<char> >&, 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

@@ -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<expr> 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;
         }