From 7eb05dd952a2f5de1d4be09436a97651c85dba18 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 2 Aug 2020 16:13:00 -0700
Subject: [PATCH] ensure lengths are registered for disequality fixe #4613
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/seq_ne_solver.cpp | 16 ++++++++++++++--
1 file changed, 14 insertions(+), 2 deletions(-)
diff --git a/src/smt/seq_ne_solver.cpp b/src/smt/seq_ne_solver.cpp
index a0519f2fe..3bb3a1151 100644
--- a/src/smt/seq_ne_solver.cpp
+++ b/src/smt/seq_ne_solver.cpp
@@ -256,8 +256,20 @@ bool theory_seq::branch_nqs() {
}
lbool theory_seq::branch_nq(ne const& n) {
-
- literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false);
+ expr_ref len_l(mk_len(n.l()), m);
+ 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);
switch (ctx.get_assignment(eq_len)) {
case l_false: