bool_rewriter: fix possible segfault when disabling rewriter.sort_dis…

[mtzguido]

…junctions

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)