mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #4080

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-23 22:58:20 -07:00
parent 6ff61d1f80
commit 7597396dd0
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smt/seq_ne_solver.cpp
View file

@ -225,9 +225,7 @@ bool theory_seq::reduce_ne(unsigned idx) {
} }
TRACE("seq", display_disequation(tout << "updated: " << updated << "\n", n); TRACE("seq", display_disequation(tout << "updated: " << updated << "\n", n););
);
if (updated) { if (updated) {
auto new_n(ne(n.l(), n.r(), new_eqs, new_lits, new_deps)); auto new_n(ne(n.l(), n.r(), new_eqs, new_lits, new_deps));
@ -247,10 +245,10 @@ bool theory_seq::branch_nqs() {
case l_undef: // needs assignment to a literal. case l_undef: // needs assignment to a literal.
return true; return true;
case l_true: // disequality is satisfied. case l_true: // disequality is satisfied.
m_nqs.erase_and_swap(i); m_nqs.erase_and_swap(i--);
break; break;
case l_false: // needs to be expanded. case l_false: // needs to be expanded.
m_nqs.erase_and_swap(i); m_nqs.erase_and_swap(i--);
return true; return true;
} }
} }
@ -264,7 +262,9 @@ lbool theory_seq::branch_nq(ne const& n) {
ctx.mark_as_relevant(eq_len); ctx.mark_as_relevant(eq_len);
switch (ctx.get_assignment(eq_len)) { switch (ctx.get_assignment(eq_len)) {
case l_false: case l_false:
TRACE("seq", ctx.display_literal_smt2(tout << "lengths are different: ", eq_len) << "\n";); TRACE("seq",
display_disequation(tout, n);
ctx.display_literal_smt2(tout << "lengths are different: ", eq_len) << "\n";);
return l_true; return l_true;
case l_undef: case l_undef:
return l_undef; return l_undef;