From 7ae706844d0bd1b47351bb1d90e8d87265f4494a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 3 Aug 2020 08:49:38 -0700
Subject: [PATCH] revert breaking change

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/seq_ne_solver.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/smt/seq_ne_solver.cpp b/src/smt/seq_ne_solver.cpp
index 3bb3a1151..dc44b52cf 100644
--- a/src/smt/seq_ne_solver.cpp
+++ b/src/smt/seq_ne_solver.cpp
@@ -258,6 +258,8 @@ bool theory_seq::branch_nqs() {
 lbool theory_seq::branch_nq(ne const& n) {
     expr_ref len_l(mk_len(n.l()), m);
     expr_ref len_r(mk_len(n.r()), m);
+#if 0
+    // TBD: breaks 
     if (!has_length(n.l())) {
         enque_axiom(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);
         return l_undef;
     }
-    
+#endif
     literal eq_len = mk_eq(len_l, len_r, false);
     ctx.mark_as_relevant(eq_len);
     switch (ctx.get_assignment(eq_len)) {