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

ensure lengths are registered for disequality fixe #4613

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

16
src/smt/seq_ne_solver.cpp
View file

@ -256,8 +256,20 @@ 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);
literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false); expr_ref len_r(mk_len(n.r()), m);
if (!has_length(n.l())) {
enque_axiom(len_l);
add_length(n.l(), len_l);
return l_undef;
}
if (!has_length(n.r())) {
enque_axiom(len_r);
add_length(n.r(), len_r);
return l_undef;
}
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)) {
case l_false: case l_false: