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

revert breaking change

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-03 08:49:38 -07:00
parent 7eb05dd952
commit 7ae706844d
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/seq_ne_solver.cpp
View file

@ -258,6 +258,8 @@ bool theory_seq::branch_nqs() {
lbool theory_seq::branch_nq(ne const& n) { lbool theory_seq::branch_nq(ne const& n) {
expr_ref len_l(mk_len(n.l()), m); expr_ref len_l(mk_len(n.l()), m);
expr_ref len_r(mk_len(n.r()), m); expr_ref len_r(mk_len(n.r()), m);
#if 0
// TBD: breaks
if (!has_length(n.l())) { if (!has_length(n.l())) {
enque_axiom(len_l); enque_axiom(len_l);
add_length(n.l(), len_l); add_length(n.l(), len_l);
@ -268,7 +270,7 @@ lbool theory_seq::branch_nq(ne const& n) {
add_length(n.r(), len_r); add_length(n.r(), len_r);
return l_undef; return l_undef;
} }
#endif
literal eq_len = mk_eq(len_l, len_r, false); literal eq_len = mk_eq(len_l, len_r, false);
ctx.mark_as_relevant(eq_len); ctx.mark_as_relevant(eq_len);
switch (ctx.get_assignment(eq_len)) { switch (ctx.get_assignment(eq_len)) {