From 64ba44d2acb12bd83941d5ec20e50e71bd199696 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 21 Jan 2021 21:01:02 -0800
Subject: [PATCH] fix underflow bug when subtracting unsigned numbers

---
 src/smt/seq_eq_solver.cpp |  4 ++--
 src/smt/theory_seq.cpp    | 48 ++++++++-------------------------------
 2 files changed, 12 insertions(+), 40 deletions(-)

diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 340ddf98e..e8b983e09 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -663,7 +663,7 @@ bool theory_seq::branch_binary_variable(eq const& e) {
     if (lenX + rational(xs.size()) != lenY + rational(ys.size())) {
         // |x| - |y| = |ys| - |xs|
         expr_ref a(mk_sub(mk_len(x), mk_len(y)), m);
-        expr_ref b(m_autil.mk_int(ys.size()-xs.size()), m);
+        expr_ref b(m_autil.mk_int(rational(ys.size())-rational(xs.size())), m);
         propagate_lit(e.dep(), 0, nullptr, mk_eq(a, b, false));
         return true;
     }
@@ -792,7 +792,7 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c
             // ls = x ++ rs ++ y, diff = |x|
             else {
                 unsigned diff = (i + 1) - rs.size();
-                for (unsigned j = 0; same && j < rs.size()-1; ++j) {
+                for (unsigned j = 0; same && j + 1 < rs.size(); ++j) {
                     same = !m.are_distinct(ls[diff + j], rs[j]);
                 }
                 if (same) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 560914881..0e876c0a9 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1267,18 +1267,11 @@ bool theory_seq::solve_nc(unsigned idx) {
     nc const& n = m_ncs[idx];
     literal len_gt = n.len_gt();
     expr_ref c(m);
-#if 1
     expr* a = nullptr, *b = nullptr;
     VERIFY(m_util.str.is_contains(n.contains(), a, b));
     literal pre, cnt, ctail, emp;
     lbool is_gt = ctx.get_assignment(len_gt);
     TRACE("seq", ctx.display_literal_smt2(tout << len_gt << " := " << is_gt << "\n", len_gt) << "\n";);
-
-#if 0
-    if (canonizes(false, n.contains())) {
-        return true;
-    }
-#endif
     
     switch (is_gt) {
     case l_true:
@@ -1292,30 +1285,8 @@ bool theory_seq::solve_nc(unsigned idx) {
     case l_false: 
         break;
     }
-#if 0
-    expr_ref a1(m), b1(m);
-    dependency* deps = n.deps();    
-    if (!canonize(a, deps, a1)) {
-        return false;
-    }
-    if (!canonize(b, deps, b1)) {
-        return false;
-    }
-    if (a != a1 || b != b1) {
-        literal_vector lits;
-        expr_ref c(m_util.str.mk_contains(a1, b1), m);
-        propagate_eq(deps, lits, c, n.contains(), false);
-        m_ncs.push_back(nc(c, len_gt, deps));       
-        m_new_propagation = true;
-        return true;
-    }
-    IF_VERBOSE(0, verbose_stream() << n.contains() << "\n");
-#endif    
     m_ax.unroll_not_contains(n.contains());
-    return true;
-    
-#endif    
-    return false;
+    return true;   
 }
 
 theory_seq::cell* theory_seq::mk_cell(cell* p, expr* e, dependency* d) {
@@ -1561,10 +1532,6 @@ void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
         return;
     if (m_sk.is_indexof_right(s))
         return;
-#if 0
-    if (m_sk.is_skolem(s))
-        return;
-#endif
     expr_ref lim_e = m_ax.add_length_limit(s, k);
     unsigned k0 = 0;
     if (m_length_limit_map.find(s, k0)) {
@@ -3182,16 +3149,16 @@ void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
         m_max_unfolding_lit = mk_literal(dlimit);        
         assumptions.push_back(dlimit);
         for (auto const& kv : m_length_limit_map) {
-            assumptions.push_back(m_sk.mk_length_limit(kv.m_key, kv.m_value));
+            if (kv.m_value > 0)
+                assumptions.push_back(m_sk.mk_length_limit(kv.m_key, kv.m_value));
         }
     }
 }
 
 bool theory_seq::should_research(expr_ref_vector & unsat_core) {
     TRACE("seq", tout << unsat_core << " " << m_util.has_re() << "\n";);
-    if (!m_has_seq) {
+    if (!m_has_seq) 
         return false;
-    }
     unsigned k_min = UINT_MAX, k = 0, n = 0;
     expr* s_min = nullptr, *s = nullptr;
     bool has_max_unfolding = false;
@@ -3210,7 +3177,8 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
             }
         }
     }
-    if (k_min < UINT_MAX) {
+
+    if (k_min < UINT_MAX/4) {
         m_max_unfolding_depth++;
         k_min *= 2;
         if (m_util.is_seq(s_min))
@@ -3224,6 +3192,10 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
         IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-depth " << m_max_unfolding_depth << ")\n");
         return true;
     }
+    else if (k_min >= UINT_MAX/4) {
+        throw default_exception("reached max unfolding");
+    }
+
     return false;
 }