diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 2548c7ab8..eef418048 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2566,31 +2566,34 @@ bool seq_rewriter::is_string(unsigned n, expr* const* es, zstring& s) const {
 
 bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs, 
                               expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
-
-    expr* l, *r;
+    expr* n = nullptr;
     is_sat = true;
-    if (szl == 1 && m_util.str.is_itos(ls[0], l)) {
-        if (szr == 1 && m_util.str.is_itos(rs[0], r)) {
-            lhs.push_back(l);
-            rhs.push_back(r);
+    if (szl == 1 && m_util.str.is_itos(ls[0], n) &&
+        solve_itos(n, szr, rs, lhs, rhs)) {
+        return true;
+    }
+    if (szr == 1 && m_util.str.is_itos(rs[0], n) &&
+        solve_itos(n, szl, ls, rhs, lhs)) {
+        return true;
+    }
+    return false;
+}
+
+/**
+ * itos(n) = <numeric string> -> n = numeric
+ */
+
+bool seq_rewriter::solve_itos(expr* n, unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs) {
+    zstring s;
+    if (is_string(sz, es, s)) {
+        std::string s1 = s.encode();
+        rational r(s1.c_str());
+        if (s1 == r.to_string()) {
+            lhs.push_back(n);
+            rhs.push_back(m_autil.mk_numeral(r, true));
             return true;
         }
-        zstring s;
-        if (is_string(szr, rs, s)) {
-            std::string s1 = s.encode();
-            rational r(s1.c_str());
-            if (s1 == r.to_string()) {
-                lhs.push_back(l);
-                rhs.push_back(m_autil.mk_numeral(r, true));
-                return true;
-            }
-        }
-    }
-
-    if (szr == 1 && szl >= 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
-        return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat);
-    }
-
+    }        
     return false;
 }
 
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 2b31c185c..6a6125095 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -153,6 +153,7 @@ class seq_rewriter {
                         expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
     bool solve_itos(unsigned n, expr* const* l, unsigned m, expr* const* r, 
                     expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
+    bool solve_itos(expr* n, unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs);
     bool min_length(unsigned n, expr* const* es, unsigned& len);
     expr* concat_non_empty(unsigned n, expr* const* es);
 
diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h
index c52477a4c..9d0f69882 100644
--- a/src/math/interval/dep_intervals.h
+++ b/src/math/interval/dep_intervals.h
@@ -209,7 +209,7 @@ public:
     }
 
     template <enum with_deps_t wd>
-        void power(const interval& a, unsigned n, interval& b) {
+    void power(const interval& a, unsigned n, interval& b) {
         if (with_deps == wd) {
             interval_deps_combine_rule combine_rule;
             m_imanager.power(a, n, b, combine_rule);
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 977622f56..59e0c81f6 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -14,6 +14,7 @@ z3_add_component(smt
     qi_queue.cpp
     seq_axioms.cpp
     seq_skolem.cpp
+    seq_eq_solver.cpp
     smt_almost_cg_table.cpp
     smt_arith_value.cpp
     smt_case_split_queue.cpp
diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index 97db818dd..ee3ebf1a7 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -120,13 +120,13 @@ void seq_axioms::add_extract_axiom(expr* e) {
     expr_ref xey = mk_concat(x, e, y);
     expr_ref zero(a.mk_int(0), m);
 
-    literal i_ge_0    = mk_literal(a.mk_ge(i, zero));
-    literal i_le_ls   = mk_literal(a.mk_le(mk_sub(i, ls), zero));
-    literal ls_le_i   = mk_literal(a.mk_le(mk_sub(ls, i), zero));
-    literal ls_ge_li  = mk_literal(a.mk_ge(ls_minus_i_l, zero));
-    literal l_ge_0    = mk_literal(a.mk_ge(l, zero));
-    literal l_le_0    = mk_literal(a.mk_le(l, zero));
-    literal ls_le_0   = mk_literal(a.mk_le(ls, zero));
+    literal i_ge_0    = mk_ge(i, zero);
+    literal i_le_ls   = mk_le(mk_sub(i, ls), zero);
+    literal ls_le_i   = mk_le(mk_sub(ls, i), zero);
+    literal ls_ge_li  = mk_ge(ls_minus_i_l, zero);
+    literal l_ge_0    = mk_ge(l, zero);
+    literal l_le_0    = mk_le(l, zero);
+    literal ls_le_0   = mk_le(ls, zero);
     literal le_is_0   = mk_eq(le, zero);
 
 
@@ -214,8 +214,8 @@ void seq_axioms::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
     expr_ref zero(a.mk_int(0), m);
     expr_ref y = m_sk.mk_post(s, l);
     expr_ref ey = mk_concat(e, y);
-    literal l_ge_0 = mk_literal(a.mk_ge(l, zero));
-    literal l_le_s = mk_literal(a.mk_le(mk_sub(l, ls), zero));
+    literal l_ge_0 = mk_ge(l, zero);
+    literal l_le_s = mk_le(mk_sub(l, ls), zero);
     add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey));
     add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le));
     add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, mk_len(y)));
@@ -236,8 +236,8 @@ void seq_axioms::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
     expr_ref zero(a.mk_int(0), m);
     expr_ref xe = mk_concat(x, e);
     literal le_is_0 = mk_eq_empty(e);
-    literal i_ge_0 = mk_literal(a.mk_ge(i, zero));
-    literal i_le_s = mk_literal(a.mk_le(mk_sub(i, ls), zero));
+    literal i_ge_0 = mk_ge(i, zero);
+    literal i_le_s = mk_le(mk_sub(i, ls), zero);
     add_axiom(~i_ge_0, ~i_le_s, mk_seq_eq(s, xe));
     add_axiom(~i_ge_0, ~i_le_s, mk_eq(i, lx));
     add_axiom(i_ge_0, le_is_0);
@@ -328,7 +328,7 @@ void seq_axioms::add_indexof_axiom(expr* i) {
         add_axiom(~s_eq_empty, i_eq_0);
         add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
         add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx));
-        add_axiom(~cnt, mk_literal(a.mk_ge(i, zero)));
+        add_axiom(~cnt, mk_ge(i, zero));
         tightest_prefix(s, x);
     }
     else {
@@ -336,8 +336,8 @@ void seq_axioms::add_indexof_axiom(expr* i) {
         // offset > len(t) => indexof(t, s, offset) = -1
         // offset = len(t) & |s| = 0 => indexof(t, s, offset) = offset
         expr_ref len_t = mk_len(t);
-        literal offset_ge_len = mk_literal(a.mk_ge(mk_sub(offset, len_t), zero));
-        literal offset_le_len = mk_literal(a.mk_le(mk_sub(offset, len_t), zero));
+        literal offset_ge_len = mk_ge(mk_sub(offset, len_t), zero);
+        literal offset_le_len = mk_le(mk_sub(offset, len_t), zero);
         literal i_eq_offset = mk_eq(i, offset);
         add_axiom(~offset_ge_len, s_eq_empty, i_eq_m1);
         add_axiom(offset_le_len, i_eq_m1);
@@ -347,7 +347,7 @@ void seq_axioms::add_indexof_axiom(expr* i) {
         expr_ref y = m_sk.mk_indexof_right(t, s, offset);
         expr_ref indexof0(seq.str.mk_index(y, s, zero), m);
         expr_ref offset_p_indexof0(a.mk_add(offset, indexof0), m);
-        literal offset_ge_0 = mk_literal(a.mk_ge(offset, zero));
+        literal offset_ge_0 = mk_ge(offset, zero);
 
         // 0 <= offset & offset < len(t) => t = xy
         // 0 <= offset & offset < len(t) => len(x) = offset
@@ -360,7 +360,7 @@ void seq_axioms::add_indexof_axiom(expr* i) {
         add_axiom(~offset_ge_0, offset_ge_len,
                   ~mk_eq(indexof0, minus_one), i_eq_m1);
         add_axiom(~offset_ge_0, offset_ge_len,
-                  ~mk_literal(a.mk_ge(indexof0, zero)),
+                  ~mk_ge(indexof0, zero),
                   mk_eq(offset_p_indexof0, i));
 
         // offset < 0 => -1 = i        
@@ -451,8 +451,8 @@ void seq_axioms::add_at_axiom(expr* e) {
     expr_ref one(a.mk_int(1), m);
     expr_ref emp(seq.str.mk_empty(m.get_sort(e)), m);
     expr_ref len_s = mk_len(s);
-    literal i_ge_0 = mk_literal(a.mk_ge(i, zero));
-    literal i_ge_len_s = mk_literal(a.mk_ge(mk_sub(i, mk_len(s)), zero));
+    literal i_ge_0 = mk_ge(i, zero);
+    literal i_ge_len_s = mk_ge(mk_sub(i, mk_len(s)), zero);
     expr_ref len_e = mk_len(e);
 
     rational iv;
@@ -480,7 +480,7 @@ void seq_axioms::add_at_axiom(expr* e) {
     add_axiom(i_ge_0, mk_eq(e, emp));
     add_axiom(~i_ge_len_s, mk_eq(e, emp));
     add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e));
-    add_axiom(mk_literal(a.mk_le(len_e, one)));
+    add_axiom(mk_le(len_e, one));
 }
 
 /**
@@ -500,8 +500,8 @@ void seq_axioms::add_nth_axiom(expr* e) {
     }
     else {
         expr_ref zero(a.mk_int(0), m);
-        literal i_ge_0 =     mk_literal(a.mk_ge(i, zero));
-        literal i_ge_len_s = mk_literal(a.mk_ge(mk_sub(i, mk_len(s)), zero));
+        literal i_ge_0 =     mk_ge(i, zero);
+        literal i_ge_len_s = mk_ge(mk_sub(i, mk_len(s)), zero);
         // at(s,i) = [nth(s,i)]
         expr_ref rhs(s, m);
         expr_ref lhs(seq.str.mk_unit(e), m);
@@ -520,12 +520,12 @@ void seq_axioms::add_itos_axiom(expr* e) {
     // itos(n) = "" <=> n < 0
     expr_ref zero(a.mk_int(0), m);
     literal eq1 = mk_literal(seq.str.mk_is_empty(e));
-    literal ge0 = mk_literal(a.mk_ge(n, zero));
+    literal ge0 = mk_ge(n, zero);
     // n >= 0 => itos(n) != ""
     // itos(n) = "" or n >= 0
     add_axiom(~eq1, ~ge0);
     add_axiom(eq1, ge0);
-    add_axiom(mk_literal(a.mk_ge(mk_len(e), zero)));    
+    add_axiom(mk_ge(mk_len(e), 0));
     
     // n >= 0 => stoi(itos(n)) = n
     app_ref stoi(seq.str.mk_stoi(e), m);
@@ -550,37 +550,74 @@ void seq_axioms::add_stoi_axiom(expr* e) {
     TRACE("seq", tout << mk_pp(e, m) << "\n";);
     expr* s = nullptr;
     VERIFY (seq.str.is_stoi(e, s));    
-    add_axiom(mk_literal(a.mk_ge(e, a.mk_int(-1))));
+    add_axiom(mk_ge(e, -1));
     add_axiom(~mk_literal(seq.str.mk_is_empty(s)), mk_eq(seq.str.mk_stoi(s), a.mk_int(-1)));   
 }
 
 /**
-   stoi(s) >= 0 => 
-          s != empty
-          s = unit(head) + tail
-          stoi(s) = 10*digit(head) + stoi(tail) or tail = empty
-          stoi(s) = digit(head) or tail != empty
-          is_digit(head)
-          (tail = empty or stoi(tail) >= 0)
+
+   stoi(s) >= 0, len(s) <= k => stoi(s) = stoi(s, k)
+   len(s) > 0  =>               stoi(s, 0) = digit(nth_i(s, 0))
+   0 < i, len(s) <= i =>        stoi(s, i) = stoi(s, i - 1)
+   0 < i, len(s) > i  =>        stoi(s, i) = 10*stoi(s, i - 1) + digit(nth_i(s, i - 1))   
+
+Define auxiliary function with the property:
+   for 0 <= i < len(s)
+     stoi(s, i) := stoi(extract(s, 0, i+1)) 
+
+   for 0 < i < len(s):
+     len(s) > i  => stoi(s, i) := stoi(extract(s, 0, i))*10 + stoi(extract(s, i, 1))
+     len(s) <= i => stoi(s, i) := stoi(extract(s, 0, i-1), i-1)
+
  */
-void seq_axioms::add_stoi_non_empty_axiom(expr* e) {
+void seq_axioms::add_stoi_axiom(expr* e, unsigned k) {
+    SASSERT(k > 0);
     expr* s = nullptr;
     VERIFY (seq.str.is_stoi(e, s));    
-    expr_ref head(m), tail(m);
-    m_sk.decompose(s, head, tail);
-    expr_ref first_char = mk_nth(s, a.mk_int(0));
-    literal ge0 = mk_literal(a.mk_ge(e, a.mk_int(0)));
-    literal tail_empty = mk_eq_empty(tail);
-    expr_ref first_digit = m_sk.mk_digit2int(first_char);
-    expr_ref stoi_tail(seq.str.mk_stoi(tail), m);
-    add_axiom(~ge0, ~mk_literal(seq.str.mk_is_empty(s)));
-    add_axiom(~ge0, mk_seq_eq(s, mk_concat(head, tail)));
-    add_axiom(~ge0, tail_empty, mk_eq(a.mk_add(a.mk_mul(a.mk_int(10), first_digit), stoi_tail), e));
-    add_axiom(~ge0, ~tail_empty, mk_eq(first_digit, e));
-    add_axiom(~ge0, is_digit(first_char));
-    add_axiom(~ge0, tail_empty, mk_literal(a.mk_ge(stoi_tail, a.mk_int(0))));    
+    auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); }; 
+    auto digit = [&](unsigned j) { return m_sk.mk_digit2int(mk_nth(s, a.mk_int(j))); };
+    expr_ref len = mk_len(s);
+    literal ge0 = mk_ge(e, 0);
+    literal lek = mk_le(len, k);
+    add_axiom(~ge0, ~mk_eq(len, a.mk_int(0)));
+    add_axiom(~ge0, ~lek, mk_eq(e, stoi2(k-1)));
+    add_axiom(mk_eq(len, a.mk_int(0)), mk_eq(stoi2(0), digit(0)));
+    for (unsigned i = 1; i < k; ++i) {
+        add_axiom(mk_le(len, i),   mk_eq(stoi2(i), a.mk_add(a.mk_mul(a.mk_int(10), stoi2(i-1)), digit(i))));
+        add_axiom(~mk_le(len, i),  mk_eq(stoi2(i), stoi2(i-1)));
+    }
 }
 
+/**
+   Let s := itos(e)
+
+   Relate values of e with len(s) where len(s) is bounded by k.
+
+   |s| = 0 => e < 0
+
+   |s| <= 1 => e < 10
+   |s| <= 2 => e < 100
+   |s| <= 3 => e < 1000
+
+   |s| >= 1 => e >= 0
+   |s| >= 2 => e >= 10
+   |s| >= 3 => e >= 100
+
+*/
+
+void seq_axioms::add_itos_axiom(expr* s, unsigned k) {
+    expr* e = nullptr;
+    VERIFY(seq.str.is_itos(s, e));
+    expr_ref len = mk_len(s);
+    add_axiom(mk_ge(e, 10), mk_le(len, 1));
+    add_axiom(mk_le(e, -1), mk_ge(len, 1));
+    rational lo(1);
+    for (unsigned i = 1; i <= k; ++i) {
+        lo *= rational(10);
+        add_axiom(mk_ge(e, lo), mk_le(len, i));
+        add_axiom(mk_le(e, lo - 1), mk_ge(len, i + 1));
+    }
+}
 
 /**
    e1 < e2 => prefix(e1, e2) or e1 = xcy e1 < e2 => prefix(e1, e2) or
@@ -644,7 +681,7 @@ void seq_axioms::add_suffix_axiom(expr* e) {
     expr* e1 = nullptr, *e2 = nullptr;
     VERIFY(seq.str.is_suffix(e, e1, e2));
     literal lit = mk_literal(e);
-    literal e1_gt_e2 = mk_literal(a.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), a.mk_int(1)));    
+    literal e1_gt_e2 = mk_ge(mk_sub(mk_len(e1), mk_len(e2)), 1);
     sort* char_sort = nullptr;
     VERIFY(seq.is_seq(m.get_sort(e1), char_sort));
     expr_ref x = m_sk.mk(symbol("seq.suffix.x"), e1, e2);
@@ -661,7 +698,7 @@ void seq_axioms::add_prefix_axiom(expr* e) {
     expr* e1 = nullptr, *e2 = nullptr;
     VERIFY(seq.str.is_prefix(e, e1, e2));
     literal lit = mk_literal(e);
-    literal e1_gt_e2 = mk_literal(a.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), a.mk_int(1)));
+    literal e1_gt_e2 = mk_ge(mk_sub(mk_len(e1), mk_len(e2)), 1);
     sort* char_sort = nullptr;
     VERIFY(seq.is_seq(m.get_sort(e1), char_sort));
     expr_ref x = m_sk.mk(symbol("seq.prefix.x"), e1, e2);
@@ -686,50 +723,6 @@ literal seq_axioms::is_digit(expr* ch) {
     add_axiom(~isd, hi);
     return isd;
 }
-// n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1
-// n >= 0 & len(e) = k => n = sum 10^i*digit(e_i)
-// n < 0  & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1
-// 10^k <= n < 10^{k+1}-1 => len(e) => k
-
-void seq_axioms::add_si_axiom(expr* e, expr* n, unsigned k) {
-    zstring s;
-    expr_ref ith_char(m), num(m), coeff(m);
-    expr_ref_vector nums(m), chars(m);
-    expr_ref len = mk_len(e);
-    literal len_eq_k = th.mk_preferred_eq(len, a.mk_int(k));
-    literal ge0 = mk_literal(a.mk_ge(n, a.mk_int(0)));
-    literal_vector digits;
-    digits.push_back(~len_eq_k);
-    digits.push_back(ge0);
-    ensure_digit_axiom();
-    for (unsigned i = 0; i < k; ++i) {
-        ith_char = mk_nth(e, a.mk_int(i));
-        literal isd = is_digit(ith_char);
-        literal len_ge_i1 = mk_literal(a.mk_ge(len, a.mk_int(i+1)));
-        add_axiom(~len_ge_i1, ~ge0, isd);
-        digits.push_back(~isd);
-        chars.push_back(seq.str.mk_unit(ith_char));
-        nums.push_back(m_sk.mk_digit2int(ith_char));
-    }        
-    ctx().mk_th_axiom(th.get_id(), digits.size(), digits.c_ptr());
-    rational c(1);
-    for (unsigned i = k; i-- > 0; c *= rational(10)) {
-        coeff = a.mk_int(c);
-        nums[i] = a.mk_mul(coeff, nums.get(i));
-    }
-    num = a.mk_add(nums.size(), nums.c_ptr());
-    m_rewrite(num);
-    add_axiom(~len_eq_k, ~ge0, th.mk_preferred_eq(n, num));
-    add_axiom(~len_eq_k, ~ge0, th.mk_preferred_eq(e, seq.str.mk_concat(chars)));
-
-    SASSERT(k > 0);
-    rational lb = power(rational(10), k - 1);
-    rational ub = power(rational(10), k) - 1;
-    literal lbl = mk_literal(a.mk_ge(n, a.mk_int(lb)));
-    literal ge_k = mk_literal(a.mk_ge(len, a.mk_int(k)));
-    // n >= lb => len(s) >= k
-    add_axiom(~lbl, ge_k);
-}
 
 void seq_axioms::ensure_digit_axiom() {
     if (!m_digits_initialized) {
@@ -745,7 +738,10 @@ void seq_axioms::ensure_digit_axiom() {
 
 expr_ref seq_axioms::add_length_limit(expr* s, unsigned k) {
     expr_ref bound_tracker  = m_sk.mk_length_limit(s, k);
-    literal bound_predicate = mk_literal(a.mk_le(mk_len(s), a.mk_int(k)));
+    expr* s0 = nullptr;
+    if (seq.str.is_stoi(s, s0)) 
+        s = s0; 
+    literal bound_predicate = mk_le(mk_len(s), k);
     add_axiom(~mk_literal(bound_tracker), bound_predicate);
     return bound_tracker;
 }
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index 8b6b57d16..df13a9c2d 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -47,6 +47,12 @@ namespace smt {
         expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(seq.str.mk_concat(e1, e2, e3), m); }
         expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(seq.str.mk_concat(e1, e2), m); }
         expr_ref mk_nth(expr* e, expr* i) { return expr_ref(seq.str.mk_nth_i(e, i), m); }
+        literal mk_ge(expr* e, int k) { return mk_ge(e, a.mk_int(k)); }
+        literal mk_le(expr* e, int k) { return mk_le(e, a.mk_int(k)); }
+        literal mk_ge(expr* e, rational const& k) { return mk_ge(e, a.mk_int(k)); }
+        literal mk_le(expr* e, rational const& k) { return mk_le(e, a.mk_int(k)); }
+        literal mk_ge(expr* x, expr* y) { return mk_literal(a.mk_ge(x, y)); }
+        literal mk_le(expr* x, expr* y) { return mk_literal(a.mk_le(x, y)); }
         void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, 
                        literal l4 = null_literal, literal l5 = null_literal) { add_axiom5(l1, l2, l3, l4, l5); }
 
@@ -78,12 +84,12 @@ namespace smt {
         void add_nth_axiom(expr* n);
         void add_itos_axiom(expr* n);
         void add_stoi_axiom(expr* n);
-        void add_stoi_non_empty_axiom(expr* e);
+        void add_stoi_axiom(expr* e, unsigned k);
+        void add_itos_axiom(expr* s, unsigned k);
         void add_lt_axiom(expr* n);
         void add_le_axiom(expr* n);
         void add_unit_axiom(expr* n);
         literal is_digit(expr* ch);
-        void add_si_axiom(expr* e, expr* n, unsigned k);
 
         expr_ref add_length_limit(expr* s, unsigned k);
     };
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
new file mode 100644
index 000000000..86e1645ca
--- /dev/null
+++ b/src/smt/seq_eq_solver.cpp
@@ -0,0 +1,1620 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    seq_eq_solver.cpp
+
+Abstract:
+
+    Features from theory_seq that are specific to solving equations.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-6-12
+*/
+
+#include <typeinfo>
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/ast_trail.h"
+#include "ast/for_each_expr.h"
+#include "smt/smt_context.h"
+#include "smt/theory_seq.h"
+#include "smt/theory_arith.h"
+
+using namespace smt;
+
+
+bool theory_seq::solve_eqs(unsigned i) {
+    context& ctx = get_context();
+    bool change = false;
+    for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
+        eq const& e = m_eqs[i];
+        if (solve_eq(e.ls(), e.rs(), e.dep(), i)) {
+            if (i + 1 != m_eqs.size()) {
+                eq e1 = m_eqs[m_eqs.size()-1];
+                m_eqs.set(i, e1);
+                --i;
+            }
+            ++m_stats.m_num_reductions;
+            m_eqs.pop_back();
+            change = true;
+        }
+        TRACE("seq_verbose", display_equations(tout););
+    }
+    return change || m_new_propagation || ctx.inconsistent();
+}
+
+bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps, unsigned idx) {
+    context& ctx = get_context();
+    expr_ref_vector& ls = m_ls;
+    expr_ref_vector& rs = m_rs;
+    rs.reset(); ls.reset();
+    dependency* dep2 = nullptr;
+    bool change = false;
+    if (!canonize(l, ls, dep2, change)) return false;
+    if (!canonize(r, rs, dep2, change)) return false;
+    deps = m_dm.mk_join(dep2, deps);
+    TRACE("seq_verbose", tout << l << " = " << r << " ==> ";
+          tout << ls << " = " << rs << "\n";
+          display_deps(tout, deps);
+          );
+    if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
+        TRACE("seq", tout << "simplified\n";);
+        return true;
+    }
+    if (!ctx.inconsistent() && lift_ite(ls, rs, deps)) {
+        return true;
+    }
+    TRACE("seq_verbose", tout << ls << " = " << rs << "\n";);
+    if (ls.empty() && rs.empty()) {
+        return true;
+    }
+    if (!ctx.inconsistent() && solve_unit_eq(ls, rs, deps)) {
+        TRACE("seq", tout << "unit\n";);
+        return true;
+    }
+    if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) {
+        TRACE("seq", tout << "binary\n";);
+        return true;
+    }
+    if (!ctx.inconsistent() && solve_nth_eq1(ls, rs, deps)) {
+        return true;
+    }
+    if (!ctx.inconsistent() && solve_nth_eq1(rs, ls, deps)) {
+        return true;
+    }
+    if (!ctx.inconsistent() && solve_itos(rs, ls, deps)) {
+        return true;
+    }
+    if (!ctx.inconsistent() && change) {
+        // The propagation step from arithmetic state (e.g. length offset) to length constraints
+        if (get_context().get_scope_level() == 0) {
+            prop_arith_to_len_offset();
+        }
+        TRACE("seq", tout << "inserting equality\n";);
+        bool updated = false;
+        if (!m_len_offset.empty()) {
+            // Find a better equivalent term for lhs of an equation based on length constraints
+            expr_ref_vector new_ls(m);
+            if (find_better_rep(ls, rs, idx, deps, new_ls)) {
+                eq const & new_eq = eq(m_eq_id++, new_ls, rs, deps);
+                m_eqs.push_back(new_eq);
+                TRACE("seq", tout << "find_better_rep\n";);
+                TRACE("seq", display_equation(tout, new_eq););
+                updated = true;
+            }
+        }
+        if (!updated) {
+            m_eqs.push_back(eq(m_eq_id++, ls, rs, deps));
+        }
+        TRACE("seq", tout << "simplified\n";);
+        return true;
+    }
+    return false;
+}
+
+// TODO: propagate length offsets for last vars
+bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned idx,
+                                 dependency*& deps, expr_ref_vector & res) {
+    context& ctx = get_context();
+
+    if (ls.empty() || rs.empty())
+        return false;
+    expr* l_fst = find_fst_non_empty_var(ls);
+    expr* r_fst = find_fst_non_empty_var(rs);
+    if (!r_fst) return false;
+    expr_ref len_r_fst = mk_len(r_fst);
+    expr_ref len_l_fst(m);
+    enode * root2;
+    if (!ctx.e_internalized(len_r_fst)) {
+        return false;
+    }
+    if (l_fst) {
+        len_l_fst = mk_len(l_fst);
+    }
+
+    root2 = get_root(len_r_fst);
+
+    // Offset = 0, No change
+    if (l_fst && get_root(len_l_fst) == root2) {
+        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
+        return false;
+    }
+
+    // Offset = 0, Changed
+
+    for (unsigned i = 0; i < idx; ++i) {
+        eq const& e = m_eqs[i];
+        if (e.ls() != ls) continue;
+        expr* nl_fst = nullptr;
+        if (e.rs().size() > 1 && is_var(e.rs().get(0)))
+            nl_fst = e.rs().get(0);
+        if (nl_fst && nl_fst != r_fst && root2 == get_root(mk_len(nl_fst))) {
+            res.reset();
+            res.append(e.rs().size(), e.rs().c_ptr());
+            deps = m_dm.mk_join(e.dep(), deps);
+            return true;
+        }
+    }
+    // Offset != 0, No change
+    if (l_fst && ctx.e_internalized(len_l_fst)) {
+        enode * root1 = get_root(len_l_fst);
+        obj_map<enode, int> tmp;
+        int offset;
+        if (!m_autil.is_numeral(root1->get_owner()) && !m_autil.is_numeral(root2->get_owner())) {
+            if (m_len_offset.find(root1, tmp) && tmp.find(root2, offset)) {
+                TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
+                find_max_eq_len(ls, rs);
+                return false;
+            }
+            else if (m_len_offset.find(root2, tmp) && tmp.find(root1, offset)) {
+                TRACE("seq", tout << "(" << mk_pp(r_fst, m) << ", " << mk_pp(l_fst,m) << ")\n";);
+                find_max_eq_len(ls ,rs);
+                return false;
+            }
+        }
+    }
+    // Offset != 0, Changed
+    obj_map<enode, int> tmp;
+    if (!m_autil.is_numeral(root2->get_owner()) && m_len_offset.find(root2, tmp)) {
+        for (unsigned i = 0; i < idx; ++i) {
+            eq const& e = m_eqs[i];
+            if (e.ls() != ls) continue;
+            expr* nl_fst = nullptr;
+            if (e.rs().size()>1 && is_var(e.rs().get(0)))
+                nl_fst = e.rs().get(0);
+            if (nl_fst && nl_fst != r_fst) {
+                int offset;
+                expr_ref len_nl_fst = mk_len(nl_fst);
+                if (ctx.e_internalized(len_nl_fst)) {
+                    enode * root1 = ctx.get_enode(len_nl_fst)->get_root();
+                    if (!m_autil.is_numeral(root1->get_owner()) && tmp.find(root1, offset)) {
+                        res.reset();
+                        res.append(e.rs().size(), e.rs().c_ptr());
+                        deps = m_dm.mk_join(e.dep(), deps);
+                        find_max_eq_len(res, rs);
+                        return true;
+                    }
+                }
+            }
+        }
+    }
+    return false;
+}
+
+bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const& rs, int & offset) {
+    context& ctx = get_context();
+
+    if (ls.empty() || rs.empty()) 
+        return false;
+    expr* l_fst = ls[0];
+    expr* r_fst = rs[0];
+    if (!is_var(l_fst) || !is_var(r_fst)) 
+        return false;
+
+    expr_ref len_l_fst = mk_len(l_fst);
+    if (!ctx.e_internalized(len_l_fst)) 
+        return false;
+    enode * root1 = ctx.get_enode(len_l_fst)->get_root();
+
+    expr_ref len_r_fst = mk_len(r_fst);
+    if (!ctx.e_internalized(len_r_fst))
+        return false;
+    enode* root2 = ctx.get_enode(len_r_fst)->get_root();
+
+    if (root1 == root2) {
+        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
+        offset = 0;
+        return true;
+    }
+
+    if (m_autil.is_numeral(root1->get_owner()) || m_autil.is_numeral(root2->get_owner())) 
+        return false;
+
+    obj_map<enode, int> tmp;
+    if (m_len_offset.find(root1, tmp) && tmp.find(root2, offset)) {
+        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
+        return true;
+    }
+    if (m_len_offset.find(root2, tmp) && tmp.find(root1, offset)) {
+        offset = -offset;
+        TRACE("seq", tout << "(" << mk_pp(r_fst, m) << ", " << mk_pp(l_fst,m) << ")\n";);
+        return true;
+    }
+    return false;
+}
+
+bool theory_seq::len_based_split() {
+    unsigned sz = m_eqs.size();
+    if (sz == 0)
+        return false;
+
+    if ((int) get_context().get_scope_level() > m_len_prop_lvl) {
+        m_len_prop_lvl = get_context().get_scope_level();
+        prop_arith_to_len_offset();
+        if (!m_len_offset.empty()) {
+            for (unsigned i = sz-1; i > 0; --i) {
+                eq const& e = m_eqs[i];
+                expr_ref_vector new_ls(m);
+                dependency *deps = e.dep();
+                if (find_better_rep(e.ls(), e.rs(), i, deps, new_ls)) {
+                    expr_ref_vector rs(m);
+                    rs.append(e.rs().size(), e.rs().c_ptr());
+                    m_eqs.set(i, eq(m_eq_id++, new_ls, rs, deps));
+                    TRACE("seq", display_equation(tout, m_eqs[i]););
+                }
+            }
+        }
+    }
+
+    for (auto const& e : m_eqs) {
+        if (len_based_split(e)) {
+            return true;
+        }
+    }
+    return false;
+}
+
+bool theory_seq::len_based_split(eq const& e) {
+    context& ctx = get_context();
+    expr_ref_vector const& ls = e.ls();
+    expr_ref_vector const& rs = e.rs();
+    
+    int offset_orig = 0;
+    if (!has_len_offset(ls, rs, offset_orig))
+        return false;
+        
+    TRACE("seq", tout << "split based on length\n";);
+    TRACE("seq", display_equation(tout, e););
+    expr_ref x11(m_util.str.mk_concat(1, ls.c_ptr()), m);
+    expr_ref x12(m_util.str.mk_concat(ls.size()-1, ls.c_ptr()+1), m);
+    expr_ref y11(m_util.str.mk_concat(1, rs.c_ptr()), m);
+    expr_ref y12(m_util.str.mk_concat(rs.size()-1, rs.c_ptr()+1), m);
+
+    expr_ref lenX11 = mk_len(x11);
+    expr_ref lenY11(m);
+    expr_ref Z(m);
+    int offset = 0;
+    if (offset_orig != 0) {
+        lenY11 = m_autil.mk_add(mk_len(y11), m_autil.mk_int(offset_orig));
+        if (offset_orig > 0) {
+            offset = offset_orig;
+            Z = m_sk.mk_align(y12, x12, x11, y11);
+            y11 = mk_concat(y11, Z);
+            x12 = mk_concat(Z, x12);
+        }
+        else {
+            offset = -offset_orig;
+            Z = m_sk.mk_align(x12, y12, y11, x11);
+            x11 = mk_concat(x11, Z);
+            y12 = mk_concat(Z, y12);
+        }
+    }
+    else {
+        lenY11 = mk_len(y11);
+    }
+
+    dependency* dep = e.dep();
+    literal_vector lits;
+    literal lit1 = mk_eq(lenX11, lenY11, false);
+    if (ctx.get_assignment(lit1) != l_true) {
+        return false;
+    }
+    lits.push_back(lit1);
+
+    if (ls.size() >= 2 && rs.size() >= 2 && (ls.size() > 2 || rs.size() > 2)) {
+        expr_ref len1(m_autil.mk_int(0),m), len2(m_autil.mk_int(0),m);
+        for (unsigned i = 2; i < ls.size(); ++i) {
+            len1 = mk_add(len1, mk_len(ls[i]));
+        }
+        for (unsigned i = 2; i < rs.size(); ++i) {
+            len2 = mk_add(len2, mk_len(rs[i]));
+        }
+        literal lit2;
+        if (!m_autil.is_numeral(len1) && !m_autil.is_numeral(len2)) {
+            lit2 = mk_eq(len1, len2, false);           
+        }
+        else {
+            expr_ref eq_len(m.mk_eq(len1, len2), m);
+            lit2 = mk_literal(eq_len);            
+        }
+        
+        if (ctx.get_assignment(lit2) == l_true) {           
+            lits.push_back(lit2);
+            TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";);
+            expr_ref lhs(m), rhs(m);
+            if (ls.size() > 2)
+                lhs = m_util.str.mk_concat(ls.size()-2, ls.c_ptr()+2);
+            else
+                lhs = m_util.str.mk_empty(m.get_sort(x11));
+            if (rs.size() > 2)
+                rhs = m_util.str.mk_concat(rs.size()-2, rs.c_ptr()+2);
+            else
+                rhs = m_util.str.mk_empty(m.get_sort(x11));
+            propagate_eq(dep, lits, lhs, rhs, true);
+            lits.pop_back();
+        }
+    }
+
+    if (offset != 0) {
+        expr_ref lenZ = mk_len(Z);
+        propagate_eq(dep, lits, lenZ, m_autil.mk_int(offset), false);
+    }
+    propagate_eq(dep, lits, y11, x11, true);
+    propagate_eq(dep, lits, x12, y12, false);
+
+    return true;
+}
+
+/**
+   \brief select branching on variable equality.
+   preference mb > eq > ternary > quat
+   this performs much better on #1628
+*/
+bool theory_seq::branch_variable() {
+    if (branch_variable_mb()) return true;
+    if (branch_variable_eq()) return true;
+    if (branch_ternary_variable1()) return true;
+    if (branch_ternary_variable2()) return true;
+    if (branch_quat_variable()) return true;
+    return false;
+}
+
+bool theory_seq::branch_variable_mb() {
+    bool change = false;
+    for (auto const& e : m_eqs) {
+        vector<rational> len1, len2;
+        if (!is_complex(e)) {
+            continue;
+        }
+        if (e.ls().empty() || e.rs().empty() || 
+            (!is_var(e.ls()[0]) && !is_var(e.rs()[0]))) {
+            continue;
+        }
+
+        if (!enforce_length(e.ls(), len1) || !enforce_length(e.rs(), len2)) {
+            // change = true;
+            continue;
+        }
+        rational l1, l2;
+        for (const auto& elem : len1) l1 += elem;
+        for (const auto& elem : len2) l2 += elem;
+        if (l1 != l2) {
+            expr_ref l = mk_concat(e.ls());
+            expr_ref r = mk_concat(e.rs());
+            expr_ref lnl = mk_len(l), lnr = mk_len(r);
+            if (propagate_eq(e.dep(), lnl, lnr, false)) {
+                change = true;
+            }
+            continue;
+        }
+        if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) {
+            TRACE("seq", tout << "split lengths\n";);
+            change = true;
+            break;
+        }
+    }
+    return change;
+}
+
+
+bool theory_seq::is_complex(eq const& e) {
+    unsigned num_vars1 = 0, num_vars2 = 0;
+    for (auto const& elem : e.ls()) {
+        if (is_var(elem)) ++num_vars1;
+    }
+    for (auto const& elem : e.rs()) {
+        if (is_var(elem)) ++num_vars2;
+    }
+    return num_vars1 > 0 && num_vars2 > 0 && num_vars1 + num_vars2 > 2;
+}
+
+/*
+  \brief Decompose ls = rs into Xa = bYc, such that 
+   1. 
+    - X != Y
+    - |b| <= |X| <= |bY| in current model
+    - b is non-empty.
+   2. X != Y
+    - b is empty
+    - |X| <= |Y|
+   3. |X| = 0
+      - propagate X = empty      
+*/
+bool theory_seq::split_lengths(dependency* dep,
+                               expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                               vector<rational> const& ll, vector<rational> const& rl) {
+    context& ctx = get_context();
+    expr_ref X(m), Y(m), b(m);
+    if (ls.empty() || rs.empty()) {
+        return false;
+    } 
+    if (is_var(ls[0]) && ll[0].is_zero()) {
+        return set_empty(ls[0]);
+    }
+    if (is_var(rs[0]) && rl[0].is_zero()) {
+        return set_empty(rs[0]);
+    }
+    if (is_var(rs[0]) && !is_var(ls[0])) {
+        return split_lengths(dep, rs, ls, rl, ll);
+    }
+    if (!is_var(ls[0])) {
+        return false;
+    }
+    X = ls[0];
+    rational lenX = ll[0];
+    expr_ref_vector bs(m);
+    SASSERT(lenX.is_pos());
+    rational lenB(0), lenY(0);
+    for (unsigned i = 0; lenX > lenB && i < rs.size(); ++i) {
+        bs.push_back(rs[i]);
+        lenY = rl[i];
+        lenB += lenY;
+    }
+    SASSERT(lenX <= lenB);
+    SASSERT(!bs.empty());
+    Y = bs.back();
+    bs.pop_back();
+    if (!is_var(Y) && !m_util.str.is_unit(Y)) {
+        TRACE("seq", tout << "TBD: non variable or unit split: " << Y << "\n";);
+        return false;
+    }
+    if (X == Y) {
+        TRACE("seq", tout << "Cycle: " << X << "\n";);
+        return false;
+    }
+    if (lenY.is_zero()) {
+        return set_empty(Y);
+    }
+    b = mk_concat(bs, m.get_sort(X));
+
+    SASSERT(X != Y);
+
+
+    // |b| < |X| <= |b| + |Y| => x = bY1, Y = Y1Y2
+    expr_ref lenXE = mk_len(X);
+    expr_ref lenYE = mk_len(Y);
+    expr_ref lenb = mk_len(b);
+    expr_ref le1(m_autil.mk_le(mk_sub(lenXE, lenb), m_autil.mk_int(0)), m);
+    expr_ref le2(m_autil.mk_le(mk_sub(mk_sub(lenXE, lenb), lenYE), 
+                               m_autil.mk_int(0)), m);
+    literal  lit1(~mk_literal(le1));
+    literal  lit2(mk_literal(le2));
+    literal_vector lits;
+    lits.push_back(lit1);
+    lits.push_back(lit2);
+    
+    if (ctx.get_assignment(lit1) != l_true ||
+        ctx.get_assignment(lit2) != l_true) {
+        ctx.mark_as_relevant(lit1);
+        ctx.mark_as_relevant(lit2);
+    }
+    else if (m_util.str.is_unit(Y)) {
+        SASSERT(lenB == lenX);
+        bs.push_back(Y);
+        expr_ref bY(m_util.str.mk_concat(bs), m);
+        propagate_eq(dep, lits, X, bY, true);
+    }
+    else {
+        SASSERT(is_var(Y));
+        expr_ref Y1 = m_sk.mk_left(X, b, Y);
+        expr_ref Y2 = m_sk.mk_right(X, b, Y);
+        TRACE("seq", tout << Y1 << "\n" << Y2 << "\n" << ls << "\n" << rs << "\n";);
+        expr_ref bY1 = mk_concat(b, Y1);
+        expr_ref Y1Y2 = mk_concat(Y1, Y2);
+        propagate_eq(dep, lits, X, bY1, true);
+        propagate_eq(dep, lits, Y, Y1Y2, true);
+    }
+    return true;
+}
+
+
+bool theory_seq::branch_binary_variable() {
+    for (auto const& e : m_eqs) {
+        if (branch_binary_variable(e)) {
+            TRACE("seq", display_equation(tout, e););
+            return true;
+        }
+    }
+    return false;
+}
+
+bool theory_seq::branch_binary_variable(eq const& e) {
+    if (is_complex(e)) {
+        return false;
+    }
+    ptr_vector<expr> xs, ys;
+    expr_ref x(m), y(m);
+    bool is_binary = is_binary_eq(e.ls(), e.rs(), x, xs, ys, y);
+    if (!is_binary) {
+        is_binary = is_binary_eq(e.rs(), e.ls(), x, xs, ys, y);
+    }
+    if (!is_binary) {
+        return false;
+    }
+    if (x == y) {
+        return false;
+    }
+        
+    // Equation is of the form x ++ xs = ys ++ y
+    // where xs, ys are units.
+    // x is either a prefix of ys, all of ys ++ y or ys ++ y1, such that y = y1 ++ y2, y2 = xs 
+    
+    rational lenX, lenY;
+    context& ctx = get_context();
+    if (branch_variable_eq(e)) {
+        return true;
+    }
+    if (!get_length(x, lenX)) {
+        add_length_to_eqc(x);
+        return true;
+    }
+    if (!get_length(y, lenY)) {
+        add_length_to_eqc(y);
+        return true;
+    }
+    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);
+        propagate_lit(e.dep(), 0, nullptr, mk_eq(a, b, false));
+        return true;
+    }
+    if (lenX <= rational(ys.size())) {
+        expr_ref_vector Ys(m);
+        Ys.append(ys.size(), ys.c_ptr());
+        branch_unit_variable(e.dep(), x, Ys);
+        return true;
+    }
+    expr_ref le(m_autil.mk_le(mk_len(x), m_autil.mk_int(ys.size())), m);
+    literal lit = mk_literal(le);
+    if (l_false == ctx.get_assignment(lit)) {
+        // |x| > |ys| => x = ys ++ y1, y = y1 ++ y2, y2 = xs
+        expr_ref Y1 = m_sk.mk_left(x, y);
+        expr_ref Y2 = m_sk.mk_right(x, y);
+        TRACE("seq", tout << Y1 << "\n" << Y2 << "\n";);
+        ys.push_back(Y1);
+        expr_ref ysY1 = mk_concat(ys);
+        expr_ref xsE = mk_concat(xs);
+        expr_ref Y1Y2 = mk_concat(Y1, Y2); 
+        dependency* dep = e.dep();
+        propagate_eq(dep, ~lit, x, ysY1);
+        propagate_eq(dep, ~lit, y, Y1Y2);
+        propagate_eq(dep, ~lit, Y2, xsE);
+    }
+    else {
+        ctx.mark_as_relevant(lit);
+    }
+    return true;
+}
+
+bool theory_seq::branch_unit_variable() {
+    bool result = false;
+    for (auto const& e : m_eqs) {
+        if (is_unit_eq(e.ls(), e.rs())) {
+            branch_unit_variable(e.dep(), e.ls()[0], e.rs());
+            result = true;
+            break;
+        }
+        else if (is_unit_eq(e.rs(), e.ls())) {
+            branch_unit_variable(e.dep(), e.rs()[0], e.ls());
+            result = true;
+            break;
+        }
+    }
+    CTRACE("seq", result, tout << "branch unit variable\n";);
+    return result;
+}
+
+void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units) {
+    SASSERT(is_var(X));
+    context& ctx = get_context();
+    rational lenX;
+    if (!get_length(X, lenX)) {
+        TRACE("seq", tout << "enforce length on " << mk_bounded_pp(X, m, 2) << "\n";);
+        add_length_to_eqc(X);
+        return;
+    }
+    if (lenX > rational(units.size())) {
+        expr_ref le(m_autil.mk_le(mk_len(X), m_autil.mk_int(units.size())), m);
+        TRACE("seq", tout << "propagate length on " << mk_bounded_pp(X, m, 2) << "\n";);
+        propagate_lit(dep, 0, nullptr, mk_literal(le));
+        return;
+    }
+    SASSERT(lenX.is_unsigned());
+    unsigned lX = lenX.get_unsigned();
+    if (lX == 0) {
+        TRACE("seq", tout << "set empty length " << mk_bounded_pp(X, m, 2) << "\n";);
+        set_empty(X);
+    }
+    else {
+        literal lit = mk_eq(m_autil.mk_int(lX), mk_len(X), false);
+        if (l_true == ctx.get_assignment(lit)) {
+            expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m);
+            propagate_eq(dep, lit, X, R);
+            TRACE("seq", tout << "propagate " << mk_pp(X, m) << " " << R << "\n";);
+        }
+        else {
+            TRACE("seq", tout << "set phase " << mk_pp(X, m) << "\n";);
+            ctx.mark_as_relevant(lit);
+            ctx.force_phase(lit);
+        }
+    }
+}
+
+bool theory_seq::branch_ternary_variable1() {
+    int start = get_context().get_random_value();
+    for (unsigned i = 0; i < m_eqs.size(); ++i) {
+        eq const& e = m_eqs[(i + start) % m_eqs.size()];
+        if (branch_ternary_variable(e) || branch_ternary_variable2(e)) {
+            return true;
+        }
+    }
+    return false;
+}
+
+bool theory_seq::branch_ternary_variable2() {
+    int start = get_context().get_random_value();
+    for (unsigned i = 0; i < m_eqs.size(); ++i) {
+        eq const& e = m_eqs[(i + start) % m_eqs.size()];
+        if (branch_ternary_variable(e, true)) {
+            return true;
+        }
+    }
+    return false;
+}
+
+bool theory_seq::eq_unit(expr* const& l, expr* const &r) const {
+    return l == r || is_unit_nth(l) || is_unit_nth(r);
+}
+
+// exists x, y, rs' != empty s.t.  (ls = x ++ rs' ++ y & rs = rs') || (ls = rs' ++ x && rs = y ++ rs')
+// TBD: spec comment above doesn't seem to match what this function does.
+unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector const& rs) {
+    SASSERT(!ls.empty() && !rs.empty());
+    unsigned_vector result;
+    expr_ref l = mk_concat(ls);
+    expr_ref r = mk_concat(rs);
+    expr_ref pair(m.mk_eq(l,r), m);
+    if (m_overlap.find(pair, result)) {
+        return result;
+    }
+    result.reset();
+    for (unsigned i = 0; i < ls.size(); ++i) {
+        if (eq_unit(ls[i], rs.back())) {
+            bool same = rs.size() > i;
+            for (unsigned j = 0; same && j < i; ++j) {
+                same = eq_unit(ls[j], rs[rs.size() - 1 - i + j]);        
+            }
+            if (same)
+                result.push_back(i+1);
+        }
+#if 0
+        if (eq_unit(ls[i], rs[0])) {
+            bool same = ls.size() - i >= rs.size();
+            for (unsigned j = 0; same && j < rs.size(); ++j) {
+                same = eq_unit(ls[i+j], rs[j]);
+            }
+            if (same)
+                result.push_back(i);
+        }
+#endif
+    }
+    m_overlap.insert(pair, result);
+    return result;
+}
+
+// exists x, y, rs' != empty s.t.  (ls = x ++ rs' ++ y & rs = rs') || (ls = x ++ rs' && rs = rs' ++ y)
+unsigned_vector theory_seq::overlap2(expr_ref_vector const& ls, expr_ref_vector const& rs) {
+    SASSERT(!ls.empty() && !rs.empty());
+    unsigned_vector res;
+    expr_ref l = mk_concat(ls);
+    expr_ref r = mk_concat(rs);
+    expr_ref pair(m.mk_eq(l,r), m);
+    if (m_overlap2.find(pair, res)) {
+        return res;
+    }
+    unsigned_vector result;
+    for (unsigned i = 0; i < ls.size(); ++i) {
+        if (eq_unit(ls[i],rs[0])) {
+            bool same = true;
+            unsigned j = i+1;
+            while (j < ls.size() && j-i < rs.size()) {
+                if (!eq_unit(ls[j], rs[j-i])) {
+                    same = false;
+                    break;
+                }
+                ++j;
+            }
+            if (same)
+                result.push_back(i);
+        }
+    }
+    m_overlap2.insert(pair, result);
+    return result;
+}
+
+bool theory_seq::branch_ternary_variable_base(
+    dependency* dep, unsigned_vector indexes,
+    expr* const& x, expr_ref_vector const& xs, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
+    context& ctx = get_context();
+    bool change = false;
+    for (auto ind : indexes) {
+        TRACE("seq", tout << "ind = " << ind << "\n";);
+        expr_ref xs2E(m);
+        if (xs.size() > ind) {
+            xs2E = m_util.str.mk_concat(xs.size()-ind, xs.c_ptr()+ind);
+        }
+        else {
+            xs2E = m_util.str.mk_empty(m.get_sort(x));
+        }
+        literal lit1 = mk_literal(m_autil.mk_le(mk_len(y2), m_autil.mk_int(xs.size()-ind)));
+        if (ctx.get_assignment(lit1) == l_undef) {
+            TRACE("seq", tout << "base case init\n";);
+            ctx.mark_as_relevant(lit1);
+            ctx.force_phase(lit1);
+            change = true;
+            continue;
+        }
+        else if (ctx.get_assignment(lit1) == l_true) {
+            TRACE("seq", tout << "base case: true branch\n";);
+            literal_vector lits;
+            lits.push_back(lit1);
+            propagate_eq(dep, lits, y2, xs2E, true);
+            if (ind > ys.size()) {
+                expr_ref xs1E(m_util.str.mk_concat(ind-ys.size(), xs.c_ptr()), m);
+                expr_ref xxs1E = mk_concat(x, xs1E);
+                propagate_eq(dep, lits, xxs1E, y1, true);
+            }
+            else if (ind == ys.size()) {
+                propagate_eq(dep, lits, x, y1, true);
+            }
+            else {
+                expr_ref ys1E(m_util.str.mk_concat(ys.size()-ind, ys.c_ptr()), m);
+                expr_ref y1ys1E = mk_concat(y1, ys1E);
+                propagate_eq(dep, lits, x, y1ys1E, true);
+            }
+            return true;
+        }
+        else {
+            TRACE("seq", tout << "base case: false branch\n";);
+            continue;
+        }
+    }
+    return change;
+}
+
+// Equation is of the form x ++ xs = y1 ++ ys ++ y2 where xs, ys are units.
+bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
+    expr_ref_vector xs(m), ys(m);
+    expr_ref x(m), y1(m), y2(m);
+    bool is_ternary = is_ternary_eq(e.ls(), e.rs(), x, xs, y1, ys, y2, flag1);
+    if (!is_ternary) {
+        is_ternary = is_ternary_eq(e.rs(), e.ls(), x, xs, y1, ys, y2, flag1);
+    }
+    if (!is_ternary) {
+        return false;
+    }
+
+    rational lenX, lenY1, lenY2;
+    context& ctx = get_context();
+    if (!get_length(x, lenX)) {
+        add_length_to_eqc(x);
+    }
+    if (!get_length(y1, lenY1)) {
+        add_length_to_eqc(y1);
+    }
+    if (!get_length(y2, lenY2)) {
+        add_length_to_eqc(y2);
+    }
+
+    SASSERT(!xs.empty() && !ys.empty());
+    unsigned_vector indexes = overlap(xs, ys);
+    if (branch_ternary_variable_base(e.dep(), indexes, x, xs, y1, ys, y2))
+        return true;
+    
+    // x ++ xs = y1 ++ ys ++ y2 => x = y1 ++ ys ++ z, z ++ xs = y2 
+    expr_ref xsE = mk_concat(xs);
+    expr_ref ysE = mk_concat(ys);
+    expr_ref y1ys = mk_concat(y1, ysE);
+    expr_ref Z = m_sk.mk_align(y2, xsE, x, y1ys);
+    expr_ref ZxsE = mk_concat(Z, xsE);
+    expr_ref y1ysZ = mk_concat(y1ys, Z);
+    if (indexes.empty()) {
+        return false;
+#if 0
+        TRACE("seq", display_equation(tout << "one case\n", e);
+              tout << "xs: " << xs << "\n";
+              tout << "ys: " << ys << "\n";);
+        literal_vector lits;
+        dependency* dep = e.dep();
+        propagate_eq(dep, lits, x, y1ysZ, true);
+        propagate_eq(dep, lits, y2, ZxsE, true);
+#endif
+    }
+    else {
+        expr_ref ge(m_autil.mk_ge(mk_len(y2), m_autil.mk_int(xs.size())), m);
+        literal lit2 = mk_literal(ge);
+        if (ctx.get_assignment(lit2) == l_undef) {
+            TRACE("seq", tout << "rec case init\n";);
+            ctx.mark_as_relevant(lit2);
+            ctx.force_phase(lit2);
+        }
+        else if (ctx.get_assignment(lit2) == l_true) {
+            TRACE("seq", tout << "true branch\n";);
+            TRACE("seq", display_equation(tout, e););
+            literal_vector lits;
+            lits.push_back(lit2);
+            dependency* dep = e.dep();
+            propagate_eq(dep, lits, x, y1ysZ, true);
+            propagate_eq(dep, lits, y2, ZxsE, true);
+        }
+        else {
+            return branch_ternary_variable_base(e.dep(), indexes, x, xs, y1, ys, y2);
+        }
+    }
+    return true;
+}
+
+bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector indexes,
+        expr_ref_vector const& xs, expr* const& x, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
+    context& ctx = get_context();
+    bool change = false;
+    for (auto ind : indexes) {
+        expr_ref xs1E(m);
+        if (ind > 0) {
+            xs1E = m_util.str.mk_concat(ind, xs.c_ptr());
+        }
+        else {
+            xs1E = m_util.str.mk_empty(m.get_sort(x));
+        }
+        literal lit1 = mk_literal(m_autil.mk_le(mk_len(y1), m_autil.mk_int(ind)));
+        if (ctx.get_assignment(lit1) == l_undef) {
+            TRACE("seq", tout << "base case init\n";);
+            ctx.mark_as_relevant(lit1);
+            ctx.force_phase(lit1);
+            change = true;
+            continue;
+        }
+        else if (ctx.get_assignment(lit1) == l_true) {
+            TRACE("seq", tout << "base case: true branch\n";);
+            literal_vector lits;
+            lits.push_back(lit1);
+            propagate_eq(dep, lits, y1, xs1E, true);
+            if (xs.size() - ind > ys.size()) {
+                expr_ref xs2E(m_util.str.mk_concat(xs.size()-ind-ys.size(), xs.c_ptr()+ind+ys.size()), m);
+                expr_ref xs2x = mk_concat(xs2E, x);
+                propagate_eq(dep, lits, xs2x, y2, true);
+            }
+            else if (xs.size() - ind == ys.size()) {
+                propagate_eq(dep, lits, x, y2, true);
+            }
+            else {
+                expr_ref ys1E(m_util.str.mk_concat(ys.size()-xs.size()+ind, ys.c_ptr()+xs.size()-ind), m);
+                expr_ref ys1y2 = mk_concat(ys1E, y2);
+                propagate_eq(dep, lits, x, ys1y2, true);
+            }
+            return true;
+        }
+        else {
+            TRACE("seq", tout << "base case: false branch\n";);
+            continue;
+        }
+    }
+    return change;
+}
+
+// Equation is of the form xs ++ x = y1 ++ ys ++ y2 where xs, ys are units.
+bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
+    expr_ref_vector xs(m), ys(m);
+    expr_ref x(m), y1(m), y2(m);
+    bool is_ternary = is_ternary_eq2(e.ls(), e.rs(), xs, x, y1, ys, y2, flag1);
+    if (!is_ternary) {
+        is_ternary = is_ternary_eq2(e.rs(), e.ls(), xs, x, y1, ys, y2, flag1);
+    }
+    if (!is_ternary) {
+        return false;
+    }
+
+    rational lenX, lenY1, lenY2;
+    context& ctx = get_context();
+    if (!get_length(x, lenX)) {
+        add_length_to_eqc(x);
+    }
+    if (!get_length(y1, lenY1)) {
+        add_length_to_eqc(y1);
+    }
+    if (!get_length(y2, lenY2)) {
+        add_length_to_eqc(y2);
+    }
+    SASSERT(!xs.empty() && !ys.empty());
+    unsigned_vector indexes = overlap2(xs, ys);
+    if (branch_ternary_variable_base2(e.dep(), indexes, xs, x, y1, ys, y2))
+        return true;
+    
+    // xs ++ x = y1 ++ ys ++ y2 => xs ++ z = y1, x = z ++ ys ++ y2 
+    expr_ref xsE = mk_concat(xs);
+    expr_ref ysE = mk_concat(ys);
+    expr_ref ysy2 = mk_concat(ysE, y2);
+    expr_ref Z = m_sk.mk_align(x, ysy2, y1, xsE);
+    expr_ref xsZ = mk_concat(xsE, Z);
+    expr_ref Zysy2 = mk_concat(Z, ysy2);
+    if (indexes.empty()) {
+        TRACE("seq", tout << "one case\n";);
+        TRACE("seq", display_equation(tout, e););
+        literal_vector lits;
+        dependency* dep = e.dep();
+        propagate_eq(dep, lits, x, Zysy2, true);
+        propagate_eq(dep, lits, y1, xsZ, true);
+    }
+    else {
+        expr_ref ge(m_autil.mk_ge(mk_len(y1), m_autil.mk_int(xs.size())), m);
+        literal lit2 = mk_literal(ge);
+        if (ctx.get_assignment(lit2) == l_undef) {
+            TRACE("seq", tout << "rec case init\n";);
+            ctx.mark_as_relevant(lit2);
+            ctx.force_phase(lit2);
+        }
+        else if (ctx.get_assignment(lit2) == l_true) {
+            TRACE("seq", tout << "true branch\n";);
+            TRACE("seq", display_equation(tout, e););
+            literal_vector lits;
+            lits.push_back(lit2);
+            dependency* dep = e.dep();
+            propagate_eq(dep, lits, x, Zysy2, true);
+            propagate_eq(dep, lits, y1, xsZ, true);
+        }
+        else {
+            return branch_ternary_variable_base2(e.dep(), indexes, xs, x, y1, ys, y2);
+        }
+    }
+
+    return true;
+}
+
+bool theory_seq::branch_quat_variable() {
+    for (auto const& e : m_eqs) {
+        if (branch_quat_variable(e)) {
+            return true;
+        }
+    }
+    return false;
+}
+
+// Equation is of the form x1 ++ xs ++ x2 = y1 ++ ys ++ y2 where xs, ys are units.
+bool theory_seq::branch_quat_variable(eq const& e) {
+    expr_ref_vector xs(m), ys(m);
+    expr_ref x1_l(m), x2(m), y1_l(m), y2(m);
+    bool is_quat = is_quat_eq(e.ls(), e.rs(), x1_l, xs, x2, y1_l, ys, y2);
+    if (!is_quat) {
+        return false;
+    }
+    
+    rational lenX1, lenX2, lenY1, lenY2;
+    context& ctx = get_context();
+    if (!get_length(x1_l, lenX1)) {
+        add_length_to_eqc(x1_l);
+    }
+    if (!get_length(y1_l, lenY1)) {
+        add_length_to_eqc(y1_l);
+    }
+    if (!get_length(x2, lenX2)) {
+        add_length_to_eqc(x2);
+    }
+    if (!get_length(y2, lenY2)) {
+        add_length_to_eqc(y2);
+    }
+    SASSERT(!xs.empty() && !ys.empty());
+    
+    xs.push_back(x2);
+    expr_ref xsx2 = mk_concat(xs);
+    ys.push_back(y2);
+    expr_ref ysy2 = mk_concat(ys);
+    expr_ref x1(x1_l, m);
+    expr_ref y1(y1_l, m);
+    expr_ref sub(mk_sub(mk_len(x1_l), mk_len(y1_l)), m);
+    expr_ref le(m_autil.mk_le(sub, m_autil.mk_int(0)), m);
+    literal lit2 = mk_literal(le);
+    if (ctx.get_assignment(lit2) == l_undef) {
+        TRACE("seq", tout << "init branch\n";);
+        TRACE("seq", display_equation(tout, e););
+        ctx.mark_as_relevant(lit2);
+        ctx.force_phase(lit2);
+    }
+    else if (ctx.get_assignment(lit2) == l_false) {
+        // |x1| > |y1| => x1 = y1 ++ z1, z1 ++ xs ++ x2 = ys ++ y2
+        TRACE("seq", tout << "false branch\n";);
+        TRACE("seq", display_equation(tout, e););
+        expr_ref Z1 = m_sk.mk_align(ysy2, xsx2, x1, y1);
+        expr_ref y1Z1 = mk_concat(y1, Z1);
+        expr_ref Z1xsx2 = mk_concat(Z1, xsx2);
+        literal_vector lits;
+        lits.push_back(~lit2);
+        dependency* dep = e.dep();
+        propagate_eq(dep, lits, x1, y1Z1, true);
+        propagate_eq(dep, lits, Z1xsx2, ysy2, true);
+    }
+    else if (ctx.get_assignment(lit2) == l_true) {
+        // |x1| <= |y1| => x1 ++ z2 = y1, xs ++ x2 = z2 ++ ys ++ y2
+        TRACE("seq", tout << "true branch\n";);
+        TRACE("seq", display_equation(tout, e););
+        expr_ref Z2 = m_sk.mk_align(xsx2, ysy2, y1, x1);
+        expr_ref x1Z2 = mk_concat(x1, Z2);
+        expr_ref Z2ysy2 = mk_concat(Z2, ysy2);
+        literal_vector lits;
+        lits.push_back(lit2);
+        dependency* dep = e.dep();
+        propagate_eq(dep, lits, x1Z2, y1, true);
+        propagate_eq(dep, lits, xsx2, Z2ysy2, true);
+    }
+    return true;
+}
+
+void theory_seq::len_offset(expr* e, rational val) {
+    context & ctx = get_context();
+    expr *l1 = nullptr, *l2 = nullptr, *l21 = nullptr, *l22 = nullptr;
+    rational fact;
+    if (m_autil.is_add(e, l1, l2) && m_autil.is_mul(l2, l21, l22) &&
+        m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
+        if (ctx.e_internalized(l1) && ctx.e_internalized(l22)) {
+            enode* r1 = get_root(l1), *n1 = r1;
+            enode* r2 = get_root(l22), *n2 = r2;
+            expr *e1 = nullptr, *e2 = nullptr;
+            do {
+                if (m_util.str.is_length(n1->get_owner(), e1))
+                    break;
+                n1 = n1->get_next();               
+            }
+            while (n1 != r1);
+            do {
+                if (m_util.str.is_length(n2->get_owner(), e2)) 
+                    break;
+                n2 = n2->get_next();                
+            }
+            while (n2 != r2);
+            obj_map<enode, int> tmp;
+            if (m_util.str.is_length(n1->get_owner(), e1)
+                && m_util.str.is_length(n2->get_owner(), e2) &&                
+                m_len_offset.find(r1, tmp)) {
+                tmp.insert(r2, val.get_int32());
+                m_len_offset.insert(r1, tmp);
+                TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";);
+                return;
+            }
+        }
+    }
+}
+
+// Find the length offset from the congruence closure core
+void theory_seq::prop_arith_to_len_offset() {
+    context & ctx = get_context();
+    obj_hashtable<enode> const_set;
+    ptr_vector<enode>::const_iterator it  = ctx.begin_enodes();
+    ptr_vector<enode>::const_iterator end = ctx.end_enodes();
+    for (; it != end; ++it) {
+        enode * root = (*it)->get_root();
+        rational val;
+        if (m_autil.is_numeral(root->get_owner(), val) && val.is_neg()) {
+            if (const_set.contains(root)) continue;
+            const_set.insert(root);
+            TRACE("seq", tout << "offset: " << mk_pp(root->get_owner(), m) << "\n";);
+            enode *next = root->get_next();
+            while (next != root) {
+                TRACE("seq", tout << "eqc: " << mk_pp(next->get_owner(), m) << "\n";);
+                len_offset(next->get_owner(), val);
+                next = next->get_next();
+            }
+        }
+    }
+}
+
+int theory_seq::find_fst_non_empty_idx(expr_ref_vector const& xs) {
+    context & ctx = get_context();    
+    for (unsigned i = 0; i < xs.size(); ++i) {
+        expr* x = xs[i];
+        if (!is_var(x)) return -1;
+        expr_ref e = mk_len(x);
+        if (ctx.e_internalized(e)) {
+            enode* root = ctx.get_enode(e)->get_root();
+            rational val;
+            if (m_autil.is_numeral(root->get_owner(), val) && val.is_zero()) {
+                continue;
+            }
+        }
+        return i;
+    }
+    return -1;
+}
+
+expr* theory_seq::find_fst_non_empty_var(expr_ref_vector const& x) {
+    int i = find_fst_non_empty_idx(x);
+    if (i >= 0)
+        return x[i];
+    return nullptr;
+}
+
+void theory_seq::find_max_eq_len(expr_ref_vector const& ls, expr_ref_vector const& rs) {
+    context& ctx = get_context();
+    if (ls.size() >= 2 && rs.size() >= 2) {
+        expr_ref len1(m_autil.mk_int(0), m), len2(m_autil.mk_int(0), m);
+        int l_fst = find_fst_non_empty_idx(ls);
+        int r_fst = find_fst_non_empty_idx(rs);
+        if (l_fst<0 || r_fst<0)
+            return;
+        unsigned j = 2 + l_fst;
+        rational lo1(-1), hi1(-1), lo2(-1), hi2(-1);
+        if (j >= ls.size()) {
+            lo1 = 0;
+            hi1 = 0;
+        }
+        while (j < ls.size()) {
+            rational lo(-1), hi(-1);
+            if (m_util.str.is_unit(ls.get(j))) {
+                lo = 1;
+                hi = 1;
+            }
+            else {
+                expr_ref len_s = mk_len(ls.get(j));
+                lower_bound(len_s, lo);
+                upper_bound(len_s, hi);
+            }
+            if (!lo.is_minus_one()) {
+                if (lo1.is_minus_one())
+                    lo1 = lo;
+                else
+                    lo1 += lo;
+            }
+            if (!hi.is_minus_one()) {
+                if (hi1.is_minus_one())
+                    hi1 = hi;
+                else if (hi1.is_nonneg())
+                    hi1 += hi;
+            }
+            else {
+                hi1 = rational(-2);
+            }
+            len1 = mk_add(len1, mk_len(ls.get(j)));
+            j++;
+        }
+        j = 2 + r_fst;
+        if (j >= rs.size()) {
+            lo2 = 0;
+            hi2 = 0;
+        }
+        while (j < rs.size()) {
+            rational lo(-1), hi(-1);
+            if (m_util.str.is_unit(rs.get(j))) {
+                lo = 1;
+                hi = 1;
+            }
+            else {
+                expr_ref len_s = mk_len(rs.get(j));
+                lower_bound(len_s, lo);
+                upper_bound(len_s, hi);
+            }
+            if (!lo.is_minus_one()) {
+                if (lo2.is_minus_one())
+                    lo2 = lo;
+                else
+                    lo2 += lo;
+            }
+            if (!hi.is_minus_one()) {
+                if (hi2.is_minus_one())
+                    hi2 = hi;
+                else if (hi1.is_nonneg())
+                    hi2 += hi;
+            }
+            else {
+                hi2 = rational(-2);
+            }
+            len2 = mk_add(len2, mk_len(rs.get(j)));
+            j++;
+        }
+        if (m_autil.is_numeral(len1) && m_autil.is_numeral(len2))
+            return;
+        TRACE("seq", tout << lo1 << ", " << hi1 << ", " << lo2 << ", " << hi2 << "\n";);
+        if (!lo1.is_neg() && !hi2.is_neg() && lo1 > hi2)
+            return;
+        if (!lo2.is_neg() && !hi1.is_neg() && lo2 > hi1)
+            return;
+
+        literal lit1 = null_literal;
+        if (hi1.is_zero()) {
+            if (!is_var(rs[1 + r_fst]))
+                return;
+            lit1 = mk_literal(m_autil.mk_le(len2, len1));
+            TRACE("seq", tout << mk_pp(len1, m) << " >= " << mk_pp(len2, m) << "\n";);
+        }
+        else if (hi2.is_zero()) {
+            if (!is_var(ls[1 + l_fst]))
+                return;
+            lit1 = mk_literal(m_autil.mk_le(len1, len2));
+            TRACE("seq", tout << mk_pp(len1, m) << " <= " << mk_pp(len2, m) << "\n";);
+        }
+        else {
+            lit1 = mk_eq(len1, len2, false);
+            TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";);
+        }
+        if (ctx.get_assignment(lit1) == l_undef) {
+            ctx.mark_as_relevant(lit1);
+            ctx.force_phase(lit1);
+        }
+    }
+}
+
+
+bool theory_seq::branch_variable_eq() {
+    context& ctx = get_context();
+    unsigned sz = m_eqs.size();
+    int start = ctx.get_random_value();
+
+    for (unsigned i = 0; i < sz; ++i) {
+        unsigned k = (i + start) % sz;
+        eq const& e = m_eqs[k];
+
+        if (branch_variable_eq(e)) {
+            TRACE("seq", tout << "branch variable\n";);
+            return true;
+        }
+    }
+    return ctx.inconsistent();
+}
+
+bool theory_seq::branch_variable_eq(eq const& e) {
+    unsigned id = e.id();
+    unsigned s = find_branch_start(2*id);
+    TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
+    bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
+    insert_branch_start(2*id, s);
+    if (found) {
+        return true;
+    }
+    s = find_branch_start(2*id + 1);
+    found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
+    insert_branch_start(2*id + 1, s);
+    
+    return found;
+}
+
+void theory_seq::insert_branch_start(unsigned k, unsigned s) {
+    m_branch_start.insert(k, s);
+    m_trail_stack.push(pop_branch(k));
+}
+
+unsigned theory_seq::find_branch_start(unsigned k) {
+    unsigned s = 0;
+    if (m_branch_start.find(k, s)) {
+        return s;
+    }
+    return 0;
+}
+
+expr_ref_vector theory_seq::expand_strings(expr_ref_vector const& es) {
+    expr_ref_vector ls(m);
+    for (expr* e : es) {
+        zstring s;
+        if (m_util.str.is_string(e, s)) {
+            for (unsigned i = 0; i < s.length(); ++i) {
+                ls.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, i)));
+            }
+        }
+        else {
+            ls.push_back(e);
+        }
+    }
+    return ls;
+}
+
+bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& _ls, expr_ref_vector const& _rs) {
+    expr_ref_vector ls = expand_strings(_ls);
+    expr_ref_vector rs = expand_strings(_rs);
+
+    if (ls.empty()) {
+        return false;
+    }
+    expr* l = ls.get(0);
+
+    if (!is_var(l)) {
+        return false;
+    }
+
+    TRACE("seq", tout << mk_pp(l, m) << ": " << get_context().get_scope_level() << " - start:" << start << "\n";);
+
+    expr_ref v0(m);
+    v0 = m_util.str.mk_empty(m.get_sort(l));
+    if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr())) {
+        if (l_false != assume_equality(l, v0)) {
+            TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
+            return true;
+        }
+    }
+    for (; start < rs.size(); ++start) {
+        unsigned j = start;
+        SASSERT(!m_util.str.is_concat(rs.get(j)));
+        SASSERT(!m_util.str.is_string(rs.get(j)));
+        if (l == rs.get(j)) {
+            return false;
+        }
+        if (!can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - j - 1, rs.c_ptr() + j + 1)) {
+            continue;
+        }
+        v0 = mk_concat(j + 1, rs.c_ptr());
+        if (l_false != assume_equality(l, v0)) {
+            TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
+            ++start;
+            return true;
+        }
+    }
+
+    bool all_units = true;
+    for (expr* r : rs) {
+        if (!m_util.str.is_unit(r)) {
+            all_units = false;
+            break;
+        }
+    }
+    if (all_units) {
+        context& ctx = get_context();
+        literal_vector lits;
+        lits.push_back(~mk_eq_empty(l));
+        for (unsigned i = 0; i < rs.size(); ++i) {
+            if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - i - 1, rs.c_ptr() + i + 1)) {
+                v0 = mk_concat(i + 1, rs.c_ptr());
+                lits.push_back(~mk_eq(l, v0, false));
+            }
+        }
+        for (literal lit : lits) {
+            switch (ctx.get_assignment(lit)) {
+            case l_true:  break;
+            case l_false: start = 0; return true;
+            case l_undef: ctx.force_phase(~lit); start = 0; return true;
+            }
+        }
+        set_conflict(dep, lits);
+        TRACE("seq", 
+              tout << "start: " << start << "\n";
+              for (literal lit : lits) {
+                  ctx.display_literal_verbose(tout << lit << ": ", lit) << "\n";
+                  ctx.display(tout, ctx.get_justification(lit.var())); tout << "\n";
+              });
+        return true;
+    }
+    return false;
+}
+
+bool theory_seq::can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const {
+    unsigned i = 0;
+    for (; i < szl && i < szr; ++i) {
+        if (m.are_distinct(ls[i], rs[i])) {
+            return false;
+        }
+        if (!m.are_equal(ls[i], rs[i])) {
+            break;
+        }
+    }
+    if (i == szr) {
+        std::swap(ls, rs);
+        std::swap(szl, szr);
+    }
+    if (i == szl && i < szr) {
+        for (; i < szr; ++i) {
+            if (m_util.str.is_unit(rs[i])) {
+                return false;
+            }
+        }
+    }
+    return true;
+}
+
+
+lbool theory_seq::assume_equality(expr* l, expr* r) {
+    context& ctx = get_context();
+    if (m_exclude.contains(l, r)) {
+        return l_false;
+    }
+
+    expr_ref eq(m.mk_eq(l, r), m);
+    m_rewrite(eq);
+    if (m.is_true(eq)) {
+        return l_true;
+    }
+    if (m.is_false(eq)) {
+        return l_false;
+    }
+
+    enode* n1 = ensure_enode(l);
+    enode* n2 = ensure_enode(r);
+    if (n1->get_root() == n2->get_root()) {
+        TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " roots eq\n";);
+        return l_true;
+    }
+    if (ctx.is_diseq(n1, n2)) {
+        TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " is_diseq\n";);
+        return l_false;
+    }
+    if (false && ctx.is_diseq_slow(n1, n2)) {
+        return l_false;
+    }
+    ctx.mark_as_relevant(n1);
+    ctx.mark_as_relevant(n2);
+    if (!ctx.assume_eq(n1, n2)) {
+        TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " can't assume\n";);
+        return l_false;
+    }
+    lbool res = ctx.get_assignment(mk_eq(l, r, false));
+    TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " literal assigned " << res << "\n";);
+    return res;
+}
+
+
+bool theory_seq::propagate_length_coherence(expr* e) {
+    expr_ref head(m), tail(m);
+    rational lo, hi;
+
+    if (!is_var(e) || !m_rep.is_root(e)) {
+        return false;
+    }
+    if (!lower_bound2(e, lo) || !lo.is_pos() || lo >= rational(2048)) {
+        return false;
+    }
+    TRACE("seq", tout << "Unsolved " << mk_pp(e, m);
+          if (!lower_bound2(e, lo)) lo = -rational::one();
+          if (!upper_bound(mk_len(e), hi)) hi = -rational::one();
+          tout << " lo: " << lo << " hi: " << hi << "\n";
+          );
+
+    expr_ref seq(e, m);
+    expr_ref_vector elems(m);
+    unsigned _lo = lo.get_unsigned();
+    for (unsigned j = 0; j < _lo; ++j) {
+        mk_decompose(seq, head, tail);
+        elems.push_back(head);
+        seq = tail;
+    }
+    expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
+    elems.push_back(seq);
+    tail = mk_concat(elems.size(), elems.c_ptr());
+    // len(e) >= low => e = tail;
+    expr_ref lo_e(m_autil.mk_numeral(lo, true), m);
+    expr_ref len_e_ge_lo(m_autil.mk_ge(mk_len(e), lo_e), m);
+    literal low = mk_literal(len_e_ge_lo);
+    add_axiom(~low, mk_seq_eq(e, tail));
+    expr_ref len_e = mk_len(e);
+    if (upper_bound(len_e, hi)) {
+        // len(e) <= hi => len(tail) <= hi - lo
+        expr_ref high1(m_autil.mk_le(len_e, m_autil.mk_numeral(hi, true)), m);
+        if (hi == lo) {
+            add_axiom(~mk_literal(high1), mk_seq_eq(seq, emp));
+        }
+        else {
+            expr_ref high2(m_autil.mk_le(mk_len(seq), m_autil.mk_numeral(hi-lo, true)), m);
+            add_axiom(~mk_literal(high1), mk_literal(high2));
+        }
+    }
+    else {
+        assume_equality(seq, emp);
+    }
+    return true;
+}
+
+
+bool theory_seq::check_length_coherence(expr* e) {
+    if (is_var(e) && m_rep.is_root(e)) {
+        if (!check_length_coherence0(e)) {
+            expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
+            expr_ref head(m), tail(m);
+            // e = emp \/ e = unit(head.elem(e))*tail(e)
+            mk_decompose(e, head, tail);
+            expr_ref conc = mk_concat(head, tail);
+            if (propagate_is_conc(e, conc)) {
+                assume_equality(tail, emp);
+            }
+        }
+        return true;
+    }
+    return false;
+}
+
+bool theory_seq::check_length_coherence0(expr* e) {
+    if (is_var(e) && m_rep.is_root(e)) {
+        expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
+        lbool r = l_false;
+        bool p = propagate_length_coherence(e);
+
+        if (!p) {
+            r = assume_equality(e, emp);
+        }
+
+        if (p || r != l_false) {
+            if (!get_context().at_base_level()) {
+                m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
+            }
+            return true;
+        }
+    }
+    return false;
+}
+
+bool theory_seq::check_length_coherence() {
+
+    for (expr* l : m_length) {
+        expr* e = nullptr;
+        VERIFY(m_util.str.is_length(l, e));
+        if (check_length_coherence0(e)) {
+            return true;
+        }
+    }
+    bool change = false;
+    unsigned sz = m_length.size();
+    for (unsigned i = 0; i < sz; ++i) {
+        expr* l = m_length.get(i);
+        expr* e = nullptr;
+        VERIFY(m_util.str.is_length(l, e));
+        if (check_length_coherence(e)) {
+            return true;
+        }
+        enode* n = ensure_enode(e);
+        enode* r = n->get_root();
+        if (r != n && has_length(r->get_owner())) {
+            continue;
+        }
+        if (add_length_to_eqc(e)) {
+            change = true;
+        }
+    }
+    return change;
+}
+
+bool theory_seq::reduce_length_eq() {
+    context& ctx = get_context();
+    int start = ctx.get_random_value();
+
+    for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
+        eq const& e = m_eqs[(i + start) % m_eqs.size()];
+        if (reduce_length_eq(e.ls(), e.rs(), e.dep())) {
+            TRACE("seq", tout << "reduce length eq\n";);
+            return true;
+        }
+    }
+    return false;
+}
+
+
+/**
+  \brief ls := X... == rs := abcdef
+*/
+bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs) {
+    if (ls.empty() || !is_var(ls[0])) {
+        return false;
+    }
+
+    for (auto const& elem : rs) {
+        if (!m_util.str.is_unit(elem)) {
+            return false;
+        }
+    }
+    return true;
+}
+
diff --git a/src/smt/seq_skolem.cpp b/src/smt/seq_skolem.cpp
index 5e1c6e448..60595bf7f 100644
--- a/src/smt/seq_skolem.cpp
+++ b/src/smt/seq_skolem.cpp
@@ -136,13 +136,18 @@ bool seq_skolem::is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, exp
     }
 }
 
-bool seq_skolem::is_tail(expr* e, expr*& s, unsigned& idx) const {
+bool seq_skolem::is_tail_u(expr* e, expr*& s, unsigned& idx) const {
     expr* i = nullptr;
     rational r;
-    return is_tail_match(e, s, i) && a.is_numeral(i, r) && r.is_unsigned() && (idx = r.get_unsigned(), true);
+    return is_tail(e, s, i) && a.is_numeral(i, r) && r.is_unsigned() && (idx = r.get_unsigned(), true);
 }
 
-bool seq_skolem::is_tail_match(expr* e, expr*& s, expr*& idx) const {
+bool seq_skolem::is_tail(expr* e, expr*& s) const {
+    expr* i = nullptr;
+    return is_tail(e, s, i);
+}
+
+bool seq_skolem::is_tail(expr* e, expr*& s, expr*& idx) const {
     return is_tail(e) && (s = to_app(e)->get_arg(0), idx = to_app(e)->get_arg(1), true);
 }
 
diff --git a/src/smt/seq_skolem.h b/src/smt/seq_skolem.h
index 306d99863..e26368403 100644
--- a/src/smt/seq_skolem.h
+++ b/src/smt/seq_skolem.h
@@ -95,8 +95,9 @@ namespace smt {
         bool is_post(expr* e, expr*& s, expr*& start);
         bool is_pre(expr* e, expr*& s, expr*& i);
         bool is_eq(expr* e, expr*& a, expr*& b) const;
-        bool is_tail_match(expr* e, expr*& s, expr*& idx) const;
-        bool is_tail(expr* e, expr*& s, unsigned& idx) const;
+        bool is_tail(expr* e, expr*& s, expr*& idx) const;
+        bool is_tail_u(expr* e, expr*& s, unsigned& idx) const;
+        bool is_tail(expr* e, expr*& s) const;
         bool is_digit(expr* e) const { return is_skolem(symbol("seq.is_digit"), e); }
         bool is_max_unfolding(expr* e) const { return is_skolem(m_max_unfolding, e); }
         bool is_length_limit(expr* e) const { return is_skolem(m_length_limit, e); }
diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index 3fda19bf1..c1e0e25fe 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -122,7 +122,7 @@ namespace smt {
             return true_literal;
         }
         context & ctx = get_context();
-        app * eq = ctx.mk_eq_atom(a, b);
+        app_ref eq(ctx.mk_eq_atom(a, b), get_manager());
         TRACE("mk_var_bug", tout << "mk_eq: " << eq->get_id() << " " << a->get_id() << " " << b->get_id() << "\n";
               tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager()););		
         ctx.internalize(eq, gate_ctx);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 944e5a9aa..8eab697f3 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -103,7 +103,6 @@ Outline:
 #include "ast/for_each_expr.h"
 #include "model/value_factory.h"
 #include "smt/smt_context.h"
-#include "smt/smt_model_generator.h"
 #include "smt/theory_seq.h"
 #include "smt/theory_arith.h"
 #include "smt/theory_lra.h"
@@ -439,1183 +438,7 @@ final_check_status theory_seq::final_check_eh() {
     return FC_GIVEUP;
 }
 
-bool theory_seq::reduce_length_eq() {
-    context& ctx = get_context();
-    int start = ctx.get_random_value();
 
-    for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
-        eq const& e = m_eqs[(i + start) % m_eqs.size()];
-        if (reduce_length_eq(e.ls(), e.rs(), e.dep())) {
-            TRACE("seq", tout << "reduce length eq\n";);
-            return true;
-        }
-    }
-    return false;
-}
-
-bool theory_seq::branch_binary_variable() {
-    for (auto const& e : m_eqs) {
-        if (branch_binary_variable(e)) {
-            TRACE("seq", display_equation(tout, e););
-            return true;
-        }
-    }
-    return false;
-}
-
-bool theory_seq::branch_binary_variable(eq const& e) {
-    if (is_complex(e)) {
-        return false;
-    }
-    ptr_vector<expr> xs, ys;
-    expr_ref x(m), y(m);
-    bool is_binary = is_binary_eq(e.ls(), e.rs(), x, xs, ys, y);
-    if (!is_binary) {
-        is_binary = is_binary_eq(e.rs(), e.ls(), x, xs, ys, y);
-    }
-    if (!is_binary) {
-        return false;
-    }
-    if (x == y) {
-        return false;
-    }
-        
-    // Equation is of the form x ++ xs = ys ++ y
-    // where xs, ys are units.
-    // x is either a prefix of ys, all of ys ++ y or ys ++ y1, such that y = y1 ++ y2, y2 = xs 
-    
-    rational lenX, lenY;
-    context& ctx = get_context();
-    if (branch_variable_eq(e)) {
-        return true;
-    }
-    if (!get_length(x, lenX)) {
-        add_length_to_eqc(x);
-        return true;
-    }
-    if (!get_length(y, lenY)) {
-        add_length_to_eqc(y);
-        return true;
-    }
-    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);
-        propagate_lit(e.dep(), 0, nullptr, mk_eq(a, b, false));
-        return true;
-    }
-    if (lenX <= rational(ys.size())) {
-        expr_ref_vector Ys(m);
-        Ys.append(ys.size(), ys.c_ptr());
-        branch_unit_variable(e.dep(), x, Ys);
-        return true;
-    }
-    expr_ref le(m_autil.mk_le(mk_len(x), m_autil.mk_int(ys.size())), m);
-    literal lit = mk_literal(le);
-    if (l_false == ctx.get_assignment(lit)) {
-        // |x| > |ys| => x = ys ++ y1, y = y1 ++ y2, y2 = xs
-        expr_ref Y1 = m_sk.mk_left(x, y);
-        expr_ref Y2 = m_sk.mk_right(x, y);
-        TRACE("seq", tout << Y1 << "\n" << Y2 << "\n";);
-        ys.push_back(Y1);
-        expr_ref ysY1 = mk_concat(ys);
-        expr_ref xsE = mk_concat(xs);
-        expr_ref Y1Y2 = mk_concat(Y1, Y2); 
-        dependency* dep = e.dep();
-        propagate_eq(dep, ~lit, x, ysY1);
-        propagate_eq(dep, ~lit, y, Y1Y2);
-        propagate_eq(dep, ~lit, Y2, xsE);
-    }
-    else {
-        ctx.mark_as_relevant(lit);
-    }
-    return true;
-}
-
-bool theory_seq::branch_unit_variable() {
-    bool result = false;
-    for (auto const& e : m_eqs) {
-        if (is_unit_eq(e.ls(), e.rs())) {
-            branch_unit_variable(e.dep(), e.ls()[0], e.rs());
-            result = true;
-            break;
-        }
-        else if (is_unit_eq(e.rs(), e.ls())) {
-            branch_unit_variable(e.dep(), e.rs()[0], e.ls());
-            result = true;
-            break;
-        }
-    }
-    CTRACE("seq", result, tout << "branch unit variable\n";);
-    return result;
-}
-
-/**
-  \brief ls := X... == rs := abcdef
-*/
-bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs) {
-    if (ls.empty() || !is_var(ls[0])) {
-        return false;
-    }
-
-    for (auto const& elem : rs) {
-        if (!m_util.str.is_unit(elem)) {
-            return false;
-        }
-    }
-    return true;
-}
-
-void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units) {
-    SASSERT(is_var(X));
-    context& ctx = get_context();
-    rational lenX;
-    if (!get_length(X, lenX)) {
-        TRACE("seq", tout << "enforce length on " << mk_bounded_pp(X, m, 2) << "\n";);
-        add_length_to_eqc(X);
-        return;
-    }
-    if (lenX > rational(units.size())) {
-        expr_ref le(m_autil.mk_le(mk_len(X), m_autil.mk_int(units.size())), m);
-        TRACE("seq", tout << "propagate length on " << mk_bounded_pp(X, m, 2) << "\n";);
-        propagate_lit(dep, 0, nullptr, mk_literal(le));
-        return;
-    }
-    SASSERT(lenX.is_unsigned());
-    unsigned lX = lenX.get_unsigned();
-    if (lX == 0) {
-        TRACE("seq", tout << "set empty length " << mk_bounded_pp(X, m, 2) << "\n";);
-        set_empty(X);
-    }
-    else {
-        literal lit = mk_eq(m_autil.mk_int(lX), mk_len(X), false);
-        if (l_true == ctx.get_assignment(lit)) {
-            expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m);
-            propagate_eq(dep, lit, X, R);
-            TRACE("seq", tout << "propagate " << mk_pp(X, m) << " " << R << "\n";);
-        }
-        else {
-            TRACE("seq", tout << "set phase " << mk_pp(X, m) << "\n";);
-            ctx.mark_as_relevant(lit);
-            ctx.force_phase(lit);
-        }
-    }
-}
-
-bool theory_seq::branch_ternary_variable1() {
-    int start = get_context().get_random_value();
-    for (unsigned i = 0; i < m_eqs.size(); ++i) {
-        eq const& e = m_eqs[(i + start) % m_eqs.size()];
-        if (branch_ternary_variable(e) || branch_ternary_variable2(e)) {
-            return true;
-        }
-    }
-    return false;
-}
-
-bool theory_seq::branch_ternary_variable2() {
-    int start = get_context().get_random_value();
-    for (unsigned i = 0; i < m_eqs.size(); ++i) {
-        eq const& e = m_eqs[(i + start) % m_eqs.size()];
-        if (branch_ternary_variable(e, true)) {
-            return true;
-        }
-    }
-    return false;
-}
-
-bool theory_seq::eq_unit(expr* const& l, expr* const &r) const {
-    return l == r || is_unit_nth(l) || is_unit_nth(r);
-}
-
-// exists x, y, rs' != empty s.t.  (ls = x ++ rs' ++ y & rs = rs') || (ls = rs' ++ x && rs = y ++ rs')
-// TBD: spec comment above doesn't seem to match what this function does.
-unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector const& rs) {
-    SASSERT(!ls.empty() && !rs.empty());
-    unsigned_vector result;
-    expr_ref l = mk_concat(ls);
-    expr_ref r = mk_concat(rs);
-    expr_ref pair(m.mk_eq(l,r), m);
-    if (m_overlap.find(pair, result)) {
-        return result;
-    }
-    result.reset();
-    for (unsigned i = 0; i < ls.size(); ++i) {
-        if (eq_unit(ls[i], rs.back())) {
-            bool same = rs.size() > i;
-            for (unsigned j = 0; same && j < i; ++j) {
-                same = eq_unit(ls[j], rs[rs.size() - 1 - i + j]);        
-            }
-            if (same)
-                result.push_back(i+1);
-        }
-#if 0
-        if (eq_unit(ls[i], rs[0])) {
-            bool same = ls.size() - i >= rs.size();
-            for (unsigned j = 0; same && j < rs.size(); ++j) {
-                same = eq_unit(ls[i+j], rs[j]);
-            }
-            if (same)
-                result.push_back(i);
-        }
-#endif
-    }
-    m_overlap.insert(pair, result);
-    return result;
-}
-
-// exists x, y, rs' != empty s.t.  (ls = x ++ rs' ++ y & rs = rs') || (ls = x ++ rs' && rs = rs' ++ y)
-unsigned_vector theory_seq::overlap2(expr_ref_vector const& ls, expr_ref_vector const& rs) {
-    SASSERT(!ls.empty() && !rs.empty());
-    unsigned_vector res;
-    expr_ref l = mk_concat(ls);
-    expr_ref r = mk_concat(rs);
-    expr_ref pair(m.mk_eq(l,r), m);
-    if (m_overlap2.find(pair, res)) {
-        return res;
-    }
-    unsigned_vector result;
-    for (unsigned i = 0; i < ls.size(); ++i) {
-        if (eq_unit(ls[i],rs[0])) {
-            bool same = true;
-            unsigned j = i+1;
-            while (j < ls.size() && j-i < rs.size()) {
-                if (!eq_unit(ls[j], rs[j-i])) {
-                    same = false;
-                    break;
-                }
-                ++j;
-            }
-            if (same)
-                result.push_back(i);
-        }
-    }
-    m_overlap2.insert(pair, result);
-    return result;
-}
-
-bool theory_seq::branch_ternary_variable_base(
-    dependency* dep, unsigned_vector indexes,
-    expr* const& x, expr_ref_vector const& xs, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
-    context& ctx = get_context();
-    bool change = false;
-    for (auto ind : indexes) {
-        TRACE("seq", tout << "ind = " << ind << "\n";);
-        expr_ref xs2E(m);
-        if (xs.size() > ind) {
-            xs2E = m_util.str.mk_concat(xs.size()-ind, xs.c_ptr()+ind);
-        }
-        else {
-            xs2E = m_util.str.mk_empty(m.get_sort(x));
-        }
-        literal lit1 = mk_literal(m_autil.mk_le(mk_len(y2), m_autil.mk_int(xs.size()-ind)));
-        if (ctx.get_assignment(lit1) == l_undef) {
-            TRACE("seq", tout << "base case init\n";);
-            ctx.mark_as_relevant(lit1);
-            ctx.force_phase(lit1);
-            change = true;
-            continue;
-        }
-        else if (ctx.get_assignment(lit1) == l_true) {
-            TRACE("seq", tout << "base case: true branch\n";);
-            literal_vector lits;
-            lits.push_back(lit1);
-            propagate_eq(dep, lits, y2, xs2E, true);
-            if (ind > ys.size()) {
-                expr_ref xs1E(m_util.str.mk_concat(ind-ys.size(), xs.c_ptr()), m);
-                expr_ref xxs1E = mk_concat(x, xs1E);
-                propagate_eq(dep, lits, xxs1E, y1, true);
-            }
-            else if (ind == ys.size()) {
-                propagate_eq(dep, lits, x, y1, true);
-            }
-            else {
-                expr_ref ys1E(m_util.str.mk_concat(ys.size()-ind, ys.c_ptr()), m);
-                expr_ref y1ys1E = mk_concat(y1, ys1E);
-                propagate_eq(dep, lits, x, y1ys1E, true);
-            }
-            return true;
-        }
-        else {
-            TRACE("seq", tout << "base case: false branch\n";);
-            continue;
-        }
-    }
-    return change;
-}
-
-// Equation is of the form x ++ xs = y1 ++ ys ++ y2 where xs, ys are units.
-bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
-    expr_ref_vector xs(m), ys(m);
-    expr_ref x(m), y1(m), y2(m);
-    bool is_ternary = is_ternary_eq(e.ls(), e.rs(), x, xs, y1, ys, y2, flag1);
-    if (!is_ternary) {
-        is_ternary = is_ternary_eq(e.rs(), e.ls(), x, xs, y1, ys, y2, flag1);
-    }
-    if (!is_ternary) {
-        return false;
-    }
-
-    rational lenX, lenY1, lenY2;
-    context& ctx = get_context();
-    if (!get_length(x, lenX)) {
-        add_length_to_eqc(x);
-    }
-    if (!get_length(y1, lenY1)) {
-        add_length_to_eqc(y1);
-    }
-    if (!get_length(y2, lenY2)) {
-        add_length_to_eqc(y2);
-    }
-
-    SASSERT(!xs.empty() && !ys.empty());
-    unsigned_vector indexes = overlap(xs, ys);
-    if (branch_ternary_variable_base(e.dep(), indexes, x, xs, y1, ys, y2))
-        return true;
-    
-    // x ++ xs = y1 ++ ys ++ y2 => x = y1 ++ ys ++ z, z ++ xs = y2 
-    expr_ref xsE = mk_concat(xs);
-    expr_ref ysE = mk_concat(ys);
-    expr_ref y1ys = mk_concat(y1, ysE);
-    expr_ref Z = m_sk.mk_align(y2, xsE, x, y1ys);
-    expr_ref ZxsE = mk_concat(Z, xsE);
-    expr_ref y1ysZ = mk_concat(y1ys, Z);
-    if (indexes.empty()) {
-        return false;
-#if 0
-        TRACE("seq", display_equation(tout << "one case\n", e);
-              tout << "xs: " << xs << "\n";
-              tout << "ys: " << ys << "\n";);
-        literal_vector lits;
-        dependency* dep = e.dep();
-        propagate_eq(dep, lits, x, y1ysZ, true);
-        propagate_eq(dep, lits, y2, ZxsE, true);
-#endif
-    }
-    else {
-        expr_ref ge(m_autil.mk_ge(mk_len(y2), m_autil.mk_int(xs.size())), m);
-        literal lit2 = mk_literal(ge);
-        if (ctx.get_assignment(lit2) == l_undef) {
-            TRACE("seq", tout << "rec case init\n";);
-            ctx.mark_as_relevant(lit2);
-            ctx.force_phase(lit2);
-        }
-        else if (ctx.get_assignment(lit2) == l_true) {
-            TRACE("seq", tout << "true branch\n";);
-            TRACE("seq", display_equation(tout, e););
-            literal_vector lits;
-            lits.push_back(lit2);
-            dependency* dep = e.dep();
-            propagate_eq(dep, lits, x, y1ysZ, true);
-            propagate_eq(dep, lits, y2, ZxsE, true);
-        }
-        else {
-            return branch_ternary_variable_base(e.dep(), indexes, x, xs, y1, ys, y2);
-        }
-    }
-    return true;
-}
-
-bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector indexes,
-        expr_ref_vector const& xs, expr* const& x, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
-    context& ctx = get_context();
-    bool change = false;
-    for (auto ind : indexes) {
-        expr_ref xs1E(m);
-        if (ind > 0) {
-            xs1E = m_util.str.mk_concat(ind, xs.c_ptr());
-        }
-        else {
-            xs1E = m_util.str.mk_empty(m.get_sort(x));
-        }
-        literal lit1 = mk_literal(m_autil.mk_le(mk_len(y1), m_autil.mk_int(ind)));
-        if (ctx.get_assignment(lit1) == l_undef) {
-            TRACE("seq", tout << "base case init\n";);
-            ctx.mark_as_relevant(lit1);
-            ctx.force_phase(lit1);
-            change = true;
-            continue;
-        }
-        else if (ctx.get_assignment(lit1) == l_true) {
-            TRACE("seq", tout << "base case: true branch\n";);
-            literal_vector lits;
-            lits.push_back(lit1);
-            propagate_eq(dep, lits, y1, xs1E, true);
-            if (xs.size() - ind > ys.size()) {
-                expr_ref xs2E(m_util.str.mk_concat(xs.size()-ind-ys.size(), xs.c_ptr()+ind+ys.size()), m);
-                expr_ref xs2x = mk_concat(xs2E, x);
-                propagate_eq(dep, lits, xs2x, y2, true);
-            }
-            else if (xs.size() - ind == ys.size()) {
-                propagate_eq(dep, lits, x, y2, true);
-            }
-            else {
-                expr_ref ys1E(m_util.str.mk_concat(ys.size()-xs.size()+ind, ys.c_ptr()+xs.size()-ind), m);
-                expr_ref ys1y2 = mk_concat(ys1E, y2);
-                propagate_eq(dep, lits, x, ys1y2, true);
-            }
-            return true;
-        }
-        else {
-            TRACE("seq", tout << "base case: false branch\n";);
-            continue;
-        }
-    }
-    return change;
-}
-
-// Equation is of the form xs ++ x = y1 ++ ys ++ y2 where xs, ys are units.
-bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
-    expr_ref_vector xs(m), ys(m);
-    expr_ref x(m), y1(m), y2(m);
-    bool is_ternary = is_ternary_eq2(e.ls(), e.rs(), xs, x, y1, ys, y2, flag1);
-    if (!is_ternary) {
-        is_ternary = is_ternary_eq2(e.rs(), e.ls(), xs, x, y1, ys, y2, flag1);
-    }
-    if (!is_ternary) {
-        return false;
-    }
-
-    rational lenX, lenY1, lenY2;
-    context& ctx = get_context();
-    if (!get_length(x, lenX)) {
-        add_length_to_eqc(x);
-    }
-    if (!get_length(y1, lenY1)) {
-        add_length_to_eqc(y1);
-    }
-    if (!get_length(y2, lenY2)) {
-        add_length_to_eqc(y2);
-    }
-    SASSERT(!xs.empty() && !ys.empty());
-    unsigned_vector indexes = overlap2(xs, ys);
-    if (branch_ternary_variable_base2(e.dep(), indexes, xs, x, y1, ys, y2))
-        return true;
-    
-    // xs ++ x = y1 ++ ys ++ y2 => xs ++ z = y1, x = z ++ ys ++ y2 
-    expr_ref xsE = mk_concat(xs);
-    expr_ref ysE = mk_concat(ys);
-    expr_ref ysy2 = mk_concat(ysE, y2);
-    expr_ref Z = m_sk.mk_align(x, ysy2, y1, xsE);
-    expr_ref xsZ = mk_concat(xsE, Z);
-    expr_ref Zysy2 = mk_concat(Z, ysy2);
-    if (indexes.empty()) {
-        TRACE("seq", tout << "one case\n";);
-        TRACE("seq", display_equation(tout, e););
-        literal_vector lits;
-        dependency* dep = e.dep();
-        propagate_eq(dep, lits, x, Zysy2, true);
-        propagate_eq(dep, lits, y1, xsZ, true);
-    }
-    else {
-        expr_ref ge(m_autil.mk_ge(mk_len(y1), m_autil.mk_int(xs.size())), m);
-        literal lit2 = mk_literal(ge);
-        if (ctx.get_assignment(lit2) == l_undef) {
-            TRACE("seq", tout << "rec case init\n";);
-            ctx.mark_as_relevant(lit2);
-            ctx.force_phase(lit2);
-        }
-        else if (ctx.get_assignment(lit2) == l_true) {
-            TRACE("seq", tout << "true branch\n";);
-            TRACE("seq", display_equation(tout, e););
-            literal_vector lits;
-            lits.push_back(lit2);
-            dependency* dep = e.dep();
-            propagate_eq(dep, lits, x, Zysy2, true);
-            propagate_eq(dep, lits, y1, xsZ, true);
-        }
-        else {
-            return branch_ternary_variable_base2(e.dep(), indexes, xs, x, y1, ys, y2);
-        }
-    }
-
-    return true;
-}
-
-bool theory_seq::branch_quat_variable() {
-    for (auto const& e : m_eqs) {
-        if (branch_quat_variable(e)) {
-            return true;
-        }
-    }
-    return false;
-}
-
-// Equation is of the form x1 ++ xs ++ x2 = y1 ++ ys ++ y2 where xs, ys are units.
-bool theory_seq::branch_quat_variable(eq const& e) {
-    expr_ref_vector xs(m), ys(m);
-    expr_ref x1_l(m), x2(m), y1_l(m), y2(m);
-    bool is_quat = is_quat_eq(e.ls(), e.rs(), x1_l, xs, x2, y1_l, ys, y2);
-    if (!is_quat) {
-        return false;
-    }
-    
-    rational lenX1, lenX2, lenY1, lenY2;
-    context& ctx = get_context();
-    if (!get_length(x1_l, lenX1)) {
-        add_length_to_eqc(x1_l);
-    }
-    if (!get_length(y1_l, lenY1)) {
-        add_length_to_eqc(y1_l);
-    }
-    if (!get_length(x2, lenX2)) {
-        add_length_to_eqc(x2);
-    }
-    if (!get_length(y2, lenY2)) {
-        add_length_to_eqc(y2);
-    }
-    SASSERT(!xs.empty() && !ys.empty());
-    
-    xs.push_back(x2);
-    expr_ref xsx2 = mk_concat(xs);
-    ys.push_back(y2);
-    expr_ref ysy2 = mk_concat(ys);
-    expr_ref x1(x1_l, m);
-    expr_ref y1(y1_l, m);
-    expr_ref sub(mk_sub(mk_len(x1_l), mk_len(y1_l)), m);
-    expr_ref le(m_autil.mk_le(sub, m_autil.mk_int(0)), m);
-    literal lit2 = mk_literal(le);
-    if (ctx.get_assignment(lit2) == l_undef) {
-        TRACE("seq", tout << "init branch\n";);
-        TRACE("seq", display_equation(tout, e););
-        ctx.mark_as_relevant(lit2);
-        ctx.force_phase(lit2);
-    }
-    else if (ctx.get_assignment(lit2) == l_false) {
-        // |x1| > |y1| => x1 = y1 ++ z1, z1 ++ xs ++ x2 = ys ++ y2
-        TRACE("seq", tout << "false branch\n";);
-        TRACE("seq", display_equation(tout, e););
-        expr_ref Z1 = m_sk.mk_align(ysy2, xsx2, x1, y1);
-        expr_ref y1Z1 = mk_concat(y1, Z1);
-        expr_ref Z1xsx2 = mk_concat(Z1, xsx2);
-        literal_vector lits;
-        lits.push_back(~lit2);
-        dependency* dep = e.dep();
-        propagate_eq(dep, lits, x1, y1Z1, true);
-        propagate_eq(dep, lits, Z1xsx2, ysy2, true);
-    }
-    else if (ctx.get_assignment(lit2) == l_true) {
-        // |x1| <= |y1| => x1 ++ z2 = y1, xs ++ x2 = z2 ++ ys ++ y2
-        TRACE("seq", tout << "true branch\n";);
-        TRACE("seq", display_equation(tout, e););
-        expr_ref Z2 = m_sk.mk_align(xsx2, ysy2, y1, x1);
-        expr_ref x1Z2 = mk_concat(x1, Z2);
-        expr_ref Z2ysy2 = mk_concat(Z2, ysy2);
-        literal_vector lits;
-        lits.push_back(lit2);
-        dependency* dep = e.dep();
-        propagate_eq(dep, lits, x1Z2, y1, true);
-        propagate_eq(dep, lits, xsx2, Z2ysy2, true);
-    }
-    return true;
-}
-
-void theory_seq::len_offset(expr* e, rational val) {
-    context & ctx = get_context();
-    expr *l1 = nullptr, *l2 = nullptr, *l21 = nullptr, *l22 = nullptr;
-    rational fact;
-    if (m_autil.is_add(e, l1, l2) && m_autil.is_mul(l2, l21, l22) &&
-        m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
-        if (ctx.e_internalized(l1) && ctx.e_internalized(l22)) {
-            enode* r1 = get_root(l1), *n1 = r1;
-            enode* r2 = get_root(l22), *n2 = r2;
-            expr *e1 = nullptr, *e2 = nullptr;
-            do {
-                if (m_util.str.is_length(n1->get_owner(), e1))
-                    break;
-                n1 = n1->get_next();               
-            }
-            while (n1 != r1);
-            do {
-                if (m_util.str.is_length(n2->get_owner(), e2)) 
-                    break;
-                n2 = n2->get_next();                
-            }
-            while (n2 != r2);
-            obj_map<enode, int> tmp;
-            if (m_util.str.is_length(n1->get_owner(), e1)
-                && m_util.str.is_length(n2->get_owner(), e2) &&                
-                m_len_offset.find(r1, tmp)) {
-                tmp.insert(r2, val.get_int32());
-                m_len_offset.insert(r1, tmp);
-                TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";);
-                return;
-            }
-        }
-    }
-}
-
-// Find the length offset from the congruence closure core
-void theory_seq::prop_arith_to_len_offset() {
-    context & ctx = get_context();
-    obj_hashtable<enode> const_set;
-    ptr_vector<enode>::const_iterator it  = ctx.begin_enodes();
-    ptr_vector<enode>::const_iterator end = ctx.end_enodes();
-    for (; it != end; ++it) {
-        enode * root = (*it)->get_root();
-        rational val;
-        if (m_autil.is_numeral(root->get_owner(), val) && val.is_neg()) {
-            if (const_set.contains(root)) continue;
-            const_set.insert(root);
-            TRACE("seq", tout << "offset: " << mk_pp(root->get_owner(), m) << "\n";);
-            enode *next = root->get_next();
-            while (next != root) {
-                TRACE("seq", tout << "eqc: " << mk_pp(next->get_owner(), m) << "\n";);
-                len_offset(next->get_owner(), val);
-                next = next->get_next();
-            }
-        }
-    }
-}
-
-int theory_seq::find_fst_non_empty_idx(expr_ref_vector const& xs) {
-    context & ctx = get_context();    
-    for (unsigned i = 0; i < xs.size(); ++i) {
-        expr* x = xs[i];
-        if (!is_var(x)) return -1;
-        expr_ref e = mk_len(x);
-        if (ctx.e_internalized(e)) {
-            enode* root = ctx.get_enode(e)->get_root();
-            rational val;
-            if (m_autil.is_numeral(root->get_owner(), val) && val.is_zero()) {
-                continue;
-            }
-        }
-        return i;
-    }
-    return -1;
-}
-
-expr* theory_seq::find_fst_non_empty_var(expr_ref_vector const& x) {
-    int i = find_fst_non_empty_idx(x);
-    if (i >= 0)
-        return x[i];
-    return nullptr;
-}
-
-void theory_seq::find_max_eq_len(expr_ref_vector const& ls, expr_ref_vector const& rs) {
-    context& ctx = get_context();
-    if (ls.size() >= 2 && rs.size() >= 2) {
-        expr_ref len1(m_autil.mk_int(0), m), len2(m_autil.mk_int(0), m);
-        int l_fst = find_fst_non_empty_idx(ls);
-        int r_fst = find_fst_non_empty_idx(rs);
-        if (l_fst<0 || r_fst<0)
-            return;
-        unsigned j = 2 + l_fst;
-        rational lo1(-1), hi1(-1), lo2(-1), hi2(-1);
-        if (j >= ls.size()) {
-            lo1 = 0;
-            hi1 = 0;
-        }
-        while (j < ls.size()) {
-            rational lo(-1), hi(-1);
-            if (m_util.str.is_unit(ls.get(j))) {
-                lo = 1;
-                hi = 1;
-            }
-            else {
-                expr_ref len_s = mk_len(ls.get(j));
-                lower_bound(len_s, lo);
-                upper_bound(len_s, hi);
-            }
-            if (!lo.is_minus_one()) {
-                if (lo1.is_minus_one())
-                    lo1 = lo;
-                else
-                    lo1 += lo;
-            }
-            if (!hi.is_minus_one()) {
-                if (hi1.is_minus_one())
-                    hi1 = hi;
-                else if (hi1.is_nonneg())
-                    hi1 += hi;
-            }
-            else {
-                hi1 = rational(-2);
-            }
-            len1 = mk_add(len1, mk_len(ls.get(j)));
-            j++;
-        }
-        j = 2 + r_fst;
-        if (j >= rs.size()) {
-            lo2 = 0;
-            hi2 = 0;
-        }
-        while (j < rs.size()) {
-            rational lo(-1), hi(-1);
-            if (m_util.str.is_unit(rs.get(j))) {
-                lo = 1;
-                hi = 1;
-            }
-            else {
-                expr_ref len_s = mk_len(rs.get(j));
-                lower_bound(len_s, lo);
-                upper_bound(len_s, hi);
-            }
-            if (!lo.is_minus_one()) {
-                if (lo2.is_minus_one())
-                    lo2 = lo;
-                else
-                    lo2 += lo;
-            }
-            if (!hi.is_minus_one()) {
-                if (hi2.is_minus_one())
-                    hi2 = hi;
-                else if (hi1.is_nonneg())
-                    hi2 += hi;
-            }
-            else {
-                hi2 = rational(-2);
-            }
-            len2 = mk_add(len2, mk_len(rs.get(j)));
-            j++;
-        }
-        if (m_autil.is_numeral(len1) && m_autil.is_numeral(len2))
-            return;
-        TRACE("seq", tout << lo1 << ", " << hi1 << ", " << lo2 << ", " << hi2 << "\n";);
-        if (!lo1.is_neg() && !hi2.is_neg() && lo1 > hi2)
-            return;
-        if (!lo2.is_neg() && !hi1.is_neg() && lo2 > hi1)
-            return;
-
-        literal lit1 = null_literal;
-        if (hi1.is_zero()) {
-            if (!is_var(rs[1 + r_fst]))
-                return;
-            lit1 = mk_literal(m_autil.mk_le(len2, len1));
-            TRACE("seq", tout << mk_pp(len1, m) << " >= " << mk_pp(len2, m) << "\n";);
-        }
-        else if (hi2.is_zero()) {
-            if (!is_var(ls[1 + l_fst]))
-                return;
-            lit1 = mk_literal(m_autil.mk_le(len1, len2));
-            TRACE("seq", tout << mk_pp(len1, m) << " <= " << mk_pp(len2, m) << "\n";);
-        }
-        else {
-            lit1 = mk_eq(len1, len2, false);
-            TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";);
-        }
-        if (ctx.get_assignment(lit1) == l_undef) {
-            ctx.mark_as_relevant(lit1);
-            ctx.force_phase(lit1);
-        }
-    }
-}
-
-// TODO: propagate length offsets for last vars
-bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned idx,
-                                 dependency*& deps, expr_ref_vector & res) {
-    context& ctx = get_context();
-
-    if (ls.empty() || rs.empty())
-        return false;
-    expr* l_fst = find_fst_non_empty_var(ls);
-    expr* r_fst = find_fst_non_empty_var(rs);
-    if (!r_fst) return false;
-    expr_ref len_r_fst = mk_len(r_fst);
-    expr_ref len_l_fst(m);
-    enode * root2;
-    if (!ctx.e_internalized(len_r_fst)) {
-        return false;
-    }
-    if (l_fst) {
-        len_l_fst = mk_len(l_fst);
-    }
-
-    root2 = get_root(len_r_fst);
-
-    // Offset = 0, No change
-    if (l_fst && get_root(len_l_fst) == root2) {
-        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
-        return false;
-    }
-
-    // Offset = 0, Changed
-
-    for (unsigned i = 0; i < idx; ++i) {
-        eq const& e = m_eqs[i];
-        if (e.ls() != ls) continue;
-        expr* nl_fst = nullptr;
-        if (e.rs().size() > 1 && is_var(e.rs().get(0)))
-            nl_fst = e.rs().get(0);
-        if (nl_fst && nl_fst != r_fst && root2 == get_root(mk_len(nl_fst))) {
-            res.reset();
-            res.append(e.rs().size(), e.rs().c_ptr());
-            deps = m_dm.mk_join(e.dep(), deps);
-            return true;
-        }
-    }
-    // Offset != 0, No change
-    if (l_fst && ctx.e_internalized(len_l_fst)) {
-        enode * root1 = get_root(len_l_fst);
-        obj_map<enode, int> tmp;
-        int offset;
-        if (!m_autil.is_numeral(root1->get_owner()) && !m_autil.is_numeral(root2->get_owner())) {
-            if (m_len_offset.find(root1, tmp) && tmp.find(root2, offset)) {
-                TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
-                find_max_eq_len(ls, rs);
-                return false;
-            }
-            else if (m_len_offset.find(root2, tmp) && tmp.find(root1, offset)) {
-                TRACE("seq", tout << "(" << mk_pp(r_fst, m) << ", " << mk_pp(l_fst,m) << ")\n";);
-                find_max_eq_len(ls ,rs);
-                return false;
-            }
-        }
-    }
-    // Offset != 0, Changed
-    obj_map<enode, int> tmp;
-    if (!m_autil.is_numeral(root2->get_owner()) && m_len_offset.find(root2, tmp)) {
-        for (unsigned i = 0; i < idx; ++i) {
-            eq const& e = m_eqs[i];
-            if (e.ls() != ls) continue;
-            expr* nl_fst = nullptr;
-            if (e.rs().size()>1 && is_var(e.rs().get(0)))
-                nl_fst = e.rs().get(0);
-            if (nl_fst && nl_fst != r_fst) {
-                int offset;
-                expr_ref len_nl_fst = mk_len(nl_fst);
-                if (ctx.e_internalized(len_nl_fst)) {
-                    enode * root1 = ctx.get_enode(len_nl_fst)->get_root();
-                    if (!m_autil.is_numeral(root1->get_owner()) && tmp.find(root1, offset)) {
-                        res.reset();
-                        res.append(e.rs().size(), e.rs().c_ptr());
-                        deps = m_dm.mk_join(e.dep(), deps);
-                        find_max_eq_len(res, rs);
-                        return true;
-                    }
-                }
-            }
-        }
-    }
-    return false;
-}
-
-bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const& rs, int & offset) {
-    context& ctx = get_context();
-
-    if (ls.empty() || rs.empty()) 
-        return false;
-    expr* l_fst = ls[0];
-    expr* r_fst = rs[0];
-    if (!is_var(l_fst) || !is_var(r_fst)) 
-        return false;
-
-    expr_ref len_l_fst = mk_len(l_fst);
-    if (!ctx.e_internalized(len_l_fst)) 
-        return false;
-    enode * root1 = ctx.get_enode(len_l_fst)->get_root();
-
-    expr_ref len_r_fst = mk_len(r_fst);
-    if (!ctx.e_internalized(len_r_fst))
-        return false;
-    enode* root2 = ctx.get_enode(len_r_fst)->get_root();
-
-    if (root1 == root2) {
-        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
-        offset = 0;
-        return true;
-    }
-
-    if (m_autil.is_numeral(root1->get_owner()) || m_autil.is_numeral(root2->get_owner())) 
-        return false;
-
-    obj_map<enode, int> tmp;
-    if (m_len_offset.find(root1, tmp) && tmp.find(root2, offset)) {
-        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
-        return true;
-    }
-    if (m_len_offset.find(root2, tmp) && tmp.find(root1, offset)) {
-        offset = -offset;
-        TRACE("seq", tout << "(" << mk_pp(r_fst, m) << ", " << mk_pp(l_fst,m) << ")\n";);
-        return true;
-    }
-    return false;
-}
-
-bool theory_seq::len_based_split() {
-    unsigned sz = m_eqs.size();
-    if (sz == 0)
-        return false;
-
-    if ((int) get_context().get_scope_level() > m_len_prop_lvl) {
-        m_len_prop_lvl = get_context().get_scope_level();
-        prop_arith_to_len_offset();
-        if (!m_len_offset.empty()) {
-            for (unsigned i = sz-1; i > 0; --i) {
-                eq const& e = m_eqs[i];
-                expr_ref_vector new_ls(m);
-                dependency *deps = e.dep();
-                if (find_better_rep(e.ls(), e.rs(), i, deps, new_ls)) {
-                    expr_ref_vector rs(m);
-                    rs.append(e.rs().size(), e.rs().c_ptr());
-                    m_eqs.set(i, eq(m_eq_id++, new_ls, rs, deps));
-                    TRACE("seq", display_equation(tout, m_eqs[i]););
-                }
-            }
-        }
-    }
-
-    for (auto const& e : m_eqs) {
-        if (len_based_split(e)) {
-            return true;
-        }
-    }
-    return false;
-}
-
-bool theory_seq::len_based_split(eq const& e) {
-    context& ctx = get_context();
-    expr_ref_vector const& ls = e.ls();
-    expr_ref_vector const& rs = e.rs();
-    
-    int offset_orig = 0;
-    if (!has_len_offset(ls, rs, offset_orig))
-        return false;
-        
-    TRACE("seq", tout << "split based on length\n";);
-    TRACE("seq", display_equation(tout, e););
-    expr_ref x11(m_util.str.mk_concat(1, ls.c_ptr()), m);
-    expr_ref x12(m_util.str.mk_concat(ls.size()-1, ls.c_ptr()+1), m);
-    expr_ref y11(m_util.str.mk_concat(1, rs.c_ptr()), m);
-    expr_ref y12(m_util.str.mk_concat(rs.size()-1, rs.c_ptr()+1), m);
-
-    expr_ref lenX11 = mk_len(x11);
-    expr_ref lenY11(m);
-    expr_ref Z(m);
-    int offset = 0;
-    if (offset_orig != 0) {
-        lenY11 = m_autil.mk_add(mk_len(y11), m_autil.mk_int(offset_orig));
-        if (offset_orig > 0) {
-            offset = offset_orig;
-            Z = m_sk.mk_align(y12, x12, x11, y11);
-            y11 = mk_concat(y11, Z);
-            x12 = mk_concat(Z, x12);
-        }
-        else {
-            offset = -offset_orig;
-            Z = m_sk.mk_align(x12, y12, y11, x11);
-            x11 = mk_concat(x11, Z);
-            y12 = mk_concat(Z, y12);
-        }
-    }
-    else {
-        lenY11 = mk_len(y11);
-    }
-
-    dependency* dep = e.dep();
-    literal_vector lits;
-    literal lit1 = mk_eq(lenX11, lenY11, false);
-    if (ctx.get_assignment(lit1) != l_true) {
-        return false;
-    }
-    lits.push_back(lit1);
-
-    if (ls.size() >= 2 && rs.size() >= 2 && (ls.size() > 2 || rs.size() > 2)) {
-        expr_ref len1(m_autil.mk_int(0),m), len2(m_autil.mk_int(0),m);
-        for (unsigned i = 2; i < ls.size(); ++i) {
-            len1 = mk_add(len1, mk_len(ls[i]));
-        }
-        for (unsigned i = 2; i < rs.size(); ++i) {
-            len2 = mk_add(len2, mk_len(rs[i]));
-        }
-        literal lit2;
-        if (!m_autil.is_numeral(len1) && !m_autil.is_numeral(len2)) {
-            lit2 = mk_eq(len1, len2, false);           
-        }
-        else {
-            expr_ref eq_len(m.mk_eq(len1, len2), m);
-            lit2 = mk_literal(eq_len);            
-        }
-        
-        if (ctx.get_assignment(lit2) == l_true) {           
-            lits.push_back(lit2);
-            TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";);
-            expr_ref lhs(m), rhs(m);
-            if (ls.size() > 2)
-                lhs = m_util.str.mk_concat(ls.size()-2, ls.c_ptr()+2);
-            else
-                lhs = m_util.str.mk_empty(m.get_sort(x11));
-            if (rs.size() > 2)
-                rhs = m_util.str.mk_concat(rs.size()-2, rs.c_ptr()+2);
-            else
-                rhs = m_util.str.mk_empty(m.get_sort(x11));
-            propagate_eq(dep, lits, lhs, rhs, true);
-            lits.pop_back();
-        }
-    }
-
-    if (offset != 0) {
-        expr_ref lenZ = mk_len(Z);
-        propagate_eq(dep, lits, lenZ, m_autil.mk_int(offset), false);
-    }
-    propagate_eq(dep, lits, y11, x11, true);
-    propagate_eq(dep, lits, x12, y12, false);
-
-    return true;
-}
-
-/**
-   \brief select branching on variable equality.
-   preference mb > eq > ternary > quat
-   this performs much better on #1628
-*/
-bool theory_seq::branch_variable() {
-    if (branch_variable_mb()) return true;
-    if (branch_variable_eq()) return true;
-    if (branch_ternary_variable1()) return true;
-    if (branch_ternary_variable2()) return true;
-    if (branch_quat_variable()) return true;
-    return false;
-}
-
-bool theory_seq::branch_variable_mb() {
-    bool change = false;
-    for (auto const& e : m_eqs) {
-        vector<rational> len1, len2;
-        if (!is_complex(e)) {
-            continue;
-        }
-        if (e.ls().empty() || e.rs().empty() || 
-            (!is_var(e.ls()[0]) && !is_var(e.rs()[0]))) {
-            continue;
-        }
-
-        if (!enforce_length(e.ls(), len1) || !enforce_length(e.rs(), len2)) {
-            // change = true;
-            continue;
-        }
-        rational l1, l2;
-        for (const auto& elem : len1) l1 += elem;
-        for (const auto& elem : len2) l2 += elem;
-        if (l1 != l2) {
-            expr_ref l = mk_concat(e.ls());
-            expr_ref r = mk_concat(e.rs());
-            expr_ref lnl = mk_len(l), lnr = mk_len(r);
-            if (propagate_eq(e.dep(), lnl, lnr, false)) {
-                change = true;
-            }
-            continue;
-        }
-        if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) {
-            TRACE("seq", tout << "split lengths\n";);
-            change = true;
-            break;
-        }
-    }
-    return change;
-}
-
-
-bool theory_seq::is_complex(eq const& e) {
-    unsigned num_vars1 = 0, num_vars2 = 0;
-    for (auto const& elem : e.ls()) {
-        if (is_var(elem)) ++num_vars1;
-    }
-    for (auto const& elem : e.rs()) {
-        if (is_var(elem)) ++num_vars2;
-    }
-    return num_vars1 > 0 && num_vars2 > 0 && num_vars1 + num_vars2 > 2;
-}
-
-/*
-  \brief Decompose ls = rs into Xa = bYc, such that 
-   1. 
-    - X != Y
-    - |b| <= |X| <= |bY| in current model
-    - b is non-empty.
-   2. X != Y
-    - b is empty
-    - |X| <= |Y|
-   3. |X| = 0
-      - propagate X = empty      
-*/
-bool theory_seq::split_lengths(dependency* dep,
-                               expr_ref_vector const& ls, expr_ref_vector const& rs, 
-                               vector<rational> const& ll, vector<rational> const& rl) {
-    context& ctx = get_context();
-    expr_ref X(m), Y(m), b(m);
-    if (ls.empty() || rs.empty()) {
-        return false;
-    } 
-    if (is_var(ls[0]) && ll[0].is_zero()) {
-        return set_empty(ls[0]);
-    }
-    if (is_var(rs[0]) && rl[0].is_zero()) {
-        return set_empty(rs[0]);
-    }
-    if (is_var(rs[0]) && !is_var(ls[0])) {
-        return split_lengths(dep, rs, ls, rl, ll);
-    }
-    if (!is_var(ls[0])) {
-        return false;
-    }
-    X = ls[0];
-    rational lenX = ll[0];
-    expr_ref_vector bs(m);
-    SASSERT(lenX.is_pos());
-    rational lenB(0), lenY(0);
-    for (unsigned i = 0; lenX > lenB && i < rs.size(); ++i) {
-        bs.push_back(rs[i]);
-        lenY = rl[i];
-        lenB += lenY;
-    }
-    SASSERT(lenX <= lenB);
-    SASSERT(!bs.empty());
-    Y = bs.back();
-    bs.pop_back();
-    if (!is_var(Y) && !m_util.str.is_unit(Y)) {
-        TRACE("seq", tout << "TBD: non variable or unit split: " << Y << "\n";);
-        return false;
-    }
-    if (X == Y) {
-        TRACE("seq", tout << "Cycle: " << X << "\n";);
-        return false;
-    }
-    if (lenY.is_zero()) {
-        return set_empty(Y);
-    }
-    b = mk_concat(bs, m.get_sort(X));
-
-    SASSERT(X != Y);
-
-
-    // |b| < |X| <= |b| + |Y| => x = bY1, Y = Y1Y2
-    expr_ref lenXE = mk_len(X);
-    expr_ref lenYE = mk_len(Y);
-    expr_ref lenb = mk_len(b);
-    expr_ref le1(m_autil.mk_le(mk_sub(lenXE, lenb), m_autil.mk_int(0)), m);
-    expr_ref le2(m_autil.mk_le(mk_sub(mk_sub(lenXE, lenb), lenYE), 
-                               m_autil.mk_int(0)), m);
-    literal  lit1(~mk_literal(le1));
-    literal  lit2(mk_literal(le2));
-    literal_vector lits;
-    lits.push_back(lit1);
-    lits.push_back(lit2);
-    
-    if (ctx.get_assignment(lit1) != l_true ||
-        ctx.get_assignment(lit2) != l_true) {
-        ctx.mark_as_relevant(lit1);
-        ctx.mark_as_relevant(lit2);
-    }
-    else if (m_util.str.is_unit(Y)) {
-        SASSERT(lenB == lenX);
-        bs.push_back(Y);
-        expr_ref bY(m_util.str.mk_concat(bs), m);
-        propagate_eq(dep, lits, X, bY, true);
-    }
-    else {
-        SASSERT(is_var(Y));
-        expr_ref Y1 = m_sk.mk_left(X, b, Y);
-        expr_ref Y2 = m_sk.mk_right(X, b, Y);
-        TRACE("seq", tout << Y1 << "\n" << Y2 << "\n" << ls << "\n" << rs << "\n";);
-        expr_ref bY1 = mk_concat(b, Y1);
-        expr_ref Y1Y2 = mk_concat(Y1, Y2);
-        propagate_eq(dep, lits, X, bY1, true);
-        propagate_eq(dep, lits, Y, Y1Y2, true);
-    }
-    return true;
-}
 
 bool theory_seq::set_empty(expr* x) {
     add_axiom(~mk_eq(m_autil.mk_int(0), mk_len(x), false), mk_eq_empty(x));
@@ -1647,327 +470,6 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & le
     return all_have_length;
 }
 
-bool theory_seq::branch_variable_eq() {
-    context& ctx = get_context();
-    unsigned sz = m_eqs.size();
-    int start = ctx.get_random_value();
-
-    for (unsigned i = 0; i < sz; ++i) {
-        unsigned k = (i + start) % sz;
-        eq const& e = m_eqs[k];
-
-        if (branch_variable_eq(e)) {
-            TRACE("seq", tout << "branch variable\n";);
-            return true;
-        }
-    }
-    return ctx.inconsistent();
-}
-
-bool theory_seq::branch_variable_eq(eq const& e) {
-    unsigned id = e.id();
-    unsigned s = find_branch_start(2*id);
-    TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
-    bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
-    insert_branch_start(2*id, s);
-    if (found) {
-        return true;
-    }
-    s = find_branch_start(2*id + 1);
-    found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
-    insert_branch_start(2*id + 1, s);
-    
-    return found;
-}
-
-void theory_seq::insert_branch_start(unsigned k, unsigned s) {
-    m_branch_start.insert(k, s);
-    m_trail_stack.push(pop_branch(k));
-}
-
-unsigned theory_seq::find_branch_start(unsigned k) {
-    unsigned s = 0;
-    if (m_branch_start.find(k, s)) {
-        return s;
-    }
-    return 0;
-}
-
-expr_ref_vector theory_seq::expand_strings(expr_ref_vector const& es) {
-    expr_ref_vector ls(m);
-    for (expr* e : es) {
-        zstring s;
-        if (m_util.str.is_string(e, s)) {
-            for (unsigned i = 0; i < s.length(); ++i) {
-                ls.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, i)));
-            }
-        }
-        else {
-            ls.push_back(e);
-        }
-    }
-    return ls;
-}
-
-bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& _ls, expr_ref_vector const& _rs) {
-    expr_ref_vector ls = expand_strings(_ls);
-    expr_ref_vector rs = expand_strings(_rs);
-
-    if (ls.empty()) {
-        return false;
-    }
-    expr* l = ls.get(0);
-
-    if (!is_var(l)) {
-        return false;
-    }
-
-    TRACE("seq", tout << mk_pp(l, m) << ": " << get_context().get_scope_level() << " - start:" << start << "\n";);
-
-    expr_ref v0(m);
-    v0 = m_util.str.mk_empty(m.get_sort(l));
-    if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr())) {
-        if (l_false != assume_equality(l, v0)) {
-            TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
-            return true;
-        }
-    }
-    for (; start < rs.size(); ++start) {
-        unsigned j = start;
-        SASSERT(!m_util.str.is_concat(rs.get(j)));
-        SASSERT(!m_util.str.is_string(rs.get(j)));
-        if (l == rs.get(j)) {
-            return false;
-        }
-        if (!can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - j - 1, rs.c_ptr() + j + 1)) {
-            continue;
-        }
-        v0 = mk_concat(j + 1, rs.c_ptr());
-        if (l_false != assume_equality(l, v0)) {
-            TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
-            ++start;
-            return true;
-        }
-    }
-
-    bool all_units = true;
-    for (expr* r : rs) {
-        if (!m_util.str.is_unit(r)) {
-            all_units = false;
-            break;
-        }
-    }
-    if (all_units) {
-        context& ctx = get_context();
-        literal_vector lits;
-        lits.push_back(~mk_eq_empty(l));
-        for (unsigned i = 0; i < rs.size(); ++i) {
-            if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - i - 1, rs.c_ptr() + i + 1)) {
-                v0 = mk_concat(i + 1, rs.c_ptr());
-                lits.push_back(~mk_eq(l, v0, false));
-            }
-        }
-        for (literal lit : lits) {
-            switch (ctx.get_assignment(lit)) {
-            case l_true:  break;
-            case l_false: start = 0; return true;
-            case l_undef: ctx.force_phase(~lit); start = 0; return true;
-            }
-        }
-        set_conflict(dep, lits);
-        TRACE("seq", 
-              tout << "start: " << start << "\n";
-              for (literal lit : lits) {
-                  ctx.display_literal_verbose(tout << lit << ": ", lit) << "\n";
-                  ctx.display(tout, ctx.get_justification(lit.var())); tout << "\n";
-              });
-        return true;
-    }
-    return false;
-}
-
-bool theory_seq::can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const {
-    unsigned i = 0;
-    for (; i < szl && i < szr; ++i) {
-        if (m.are_distinct(ls[i], rs[i])) {
-            return false;
-        }
-        if (!m.are_equal(ls[i], rs[i])) {
-            break;
-        }
-    }
-    if (i == szr) {
-        std::swap(ls, rs);
-        std::swap(szl, szr);
-    }
-    if (i == szl && i < szr) {
-        for (; i < szr; ++i) {
-            if (m_util.str.is_unit(rs[i])) {
-                return false;
-            }
-        }
-    }
-    return true;
-}
-
-
-lbool theory_seq::assume_equality(expr* l, expr* r) {
-    context& ctx = get_context();
-    if (m_exclude.contains(l, r)) {
-        return l_false;
-    }
-
-    expr_ref eq(m.mk_eq(l, r), m);
-    m_rewrite(eq);
-    if (m.is_true(eq)) {
-        return l_true;
-    }
-    if (m.is_false(eq)) {
-        return l_false;
-    }
-
-    enode* n1 = ensure_enode(l);
-    enode* n2 = ensure_enode(r);
-    if (n1->get_root() == n2->get_root()) {
-        TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " roots eq\n";);
-        return l_true;
-    }
-    if (ctx.is_diseq(n1, n2)) {
-        TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " is_diseq\n";);
-        return l_false;
-    }
-    if (false && ctx.is_diseq_slow(n1, n2)) {
-        return l_false;
-    }
-    ctx.mark_as_relevant(n1);
-    ctx.mark_as_relevant(n2);
-    if (!ctx.assume_eq(n1, n2)) {
-        TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " can't assume\n";);
-        return l_false;
-    }
-    lbool res = ctx.get_assignment(mk_eq(l, r, false));
-    TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " literal assigned " << res << "\n";);
-    return res;
-}
-
-
-bool theory_seq::propagate_length_coherence(expr* e) {
-    expr_ref head(m), tail(m);
-    rational lo, hi;
-
-    if (!is_var(e) || !m_rep.is_root(e)) {
-        return false;
-    }
-    if (!lower_bound2(e, lo) || !lo.is_pos() || lo >= rational(2048)) {
-        return false;
-    }
-    TRACE("seq", tout << "Unsolved " << mk_pp(e, m);
-          if (!lower_bound2(e, lo)) lo = -rational::one();
-          if (!upper_bound(mk_len(e), hi)) hi = -rational::one();
-          tout << " lo: " << lo << " hi: " << hi << "\n";
-          );
-
-    expr_ref seq(e, m);
-    expr_ref_vector elems(m);
-    unsigned _lo = lo.get_unsigned();
-    for (unsigned j = 0; j < _lo; ++j) {
-        mk_decompose(seq, head, tail);
-        elems.push_back(head);
-        seq = tail;
-    }
-    expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
-    elems.push_back(seq);
-    tail = mk_concat(elems.size(), elems.c_ptr());
-    // len(e) >= low => e = tail;
-    expr_ref lo_e(m_autil.mk_numeral(lo, true), m);
-    expr_ref len_e_ge_lo(m_autil.mk_ge(mk_len(e), lo_e), m);
-    literal low = mk_literal(len_e_ge_lo);
-    add_axiom(~low, mk_seq_eq(e, tail));
-    expr_ref len_e = mk_len(e);
-    if (upper_bound(len_e, hi)) {
-        // len(e) <= hi => len(tail) <= hi - lo
-        expr_ref high1(m_autil.mk_le(len_e, m_autil.mk_numeral(hi, true)), m);
-        if (hi == lo) {
-            add_axiom(~mk_literal(high1), mk_seq_eq(seq, emp));
-        }
-        else {
-            expr_ref high2(m_autil.mk_le(mk_len(seq), m_autil.mk_numeral(hi-lo, true)), m);
-            add_axiom(~mk_literal(high1), mk_literal(high2));
-        }
-    }
-    else {
-        assume_equality(seq, emp);
-    }
-    return true;
-}
-
-
-bool theory_seq::check_length_coherence(expr* e) {
-    if (is_var(e) && m_rep.is_root(e)) {
-        if (!check_length_coherence0(e)) {
-            expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
-            expr_ref head(m), tail(m);
-            // e = emp \/ e = unit(head.elem(e))*tail(e)
-            mk_decompose(e, head, tail);
-            expr_ref conc = mk_concat(head, tail);
-            if (propagate_is_conc(e, conc)) {
-                assume_equality(tail, emp);
-            }
-        }
-        return true;
-    }
-    return false;
-}
-
-bool theory_seq::check_length_coherence0(expr* e) {
-    if (is_var(e) && m_rep.is_root(e)) {
-        expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
-        lbool r = l_false;
-        bool p = propagate_length_coherence(e);
-
-        if (!p) {
-            r = assume_equality(e, emp);
-        }
-
-        if (p || r != l_false) {
-            if (!get_context().at_base_level()) {
-                m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
-            }
-            return true;
-        }
-    }
-    return false;
-}
-
-bool theory_seq::check_length_coherence() {
-
-    for (expr* l : m_length) {
-        expr* e = nullptr;
-        VERIFY(m_util.str.is_length(l, e));
-        if (check_length_coherence0(e)) {
-            return true;
-        }
-    }
-    bool change = false;
-    unsigned sz = m_length.size();
-    for (unsigned i = 0; i < sz; ++i) {
-        expr* l = m_length.get(i);
-        expr* e = nullptr;
-        VERIFY(m_util.str.is_length(l, e));
-        if (check_length_coherence(e)) {
-            return true;
-        }
-        enode* n = ensure_enode(e);
-        enode* r = n->get_root();
-        if (r != n && has_length(r->get_owner())) {
-            continue;
-        }
-        if (add_length_to_eqc(e)) {
-            change = true;
-        }
-    }
-    return change;
-}
 
 bool theory_seq::fixed_length(bool is_zero) {
     bool found = false;    
@@ -2465,19 +967,42 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
 
 bool theory_seq::solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
     expr* e = nullptr;
-    if (ls.size() == 1 && rs.empty() && m_util.str.is_itos(ls[0], e)) {
-        literal lit = mk_simplified_literal(m_autil.mk_le(e, m_autil.mk_int(-1)));
-        propagate_lit(dep, 0, nullptr, lit);
+    
+    if (rs.size() == 1 && m_util.str.is_itos(rs[0], e) && solve_itos(e, ls, dep))
         return true;
-    } 
-    if (rs.size() == 1 && ls.empty() && m_util.str.is_itos(rs[0], e)) {
-        literal lit = mk_simplified_literal(m_autil.mk_le(e, m_autil.mk_int(-1)));
-        propagate_lit(dep, 0, nullptr, lit);
+    if (ls.size() == 1 && m_util.str.is_itos(ls[0], e) && solve_itos(e, rs, dep)) 
         return true;
-    } 
     return false;
 }
 
+bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep) {
+    if (rs.empty()) {
+        literal lit = mk_simplified_literal(m_autil.mk_le(n, m_autil.mk_int(-1)));
+        propagate_lit(dep, 0, nullptr, lit);
+        return true;
+    } 
+    expr_ref num(m), digit(m);
+    expr* u = nullptr;
+    for (expr* r : rs) {
+        if (!m_util.str.is_unit(r, u))
+            return false;
+        digit = m_sk.mk_digit2int(u);
+        if (!num) {
+            num = digit;
+        }
+        else {
+            num = m_autil.mk_add(m_autil.mk_mul(m_autil.mk_int(10), num), digit);
+        }
+    }
+    propagate_lit(dep, 0, nullptr, mk_simplified_literal(m.mk_eq(n, num)));
+    if (rs.size() > 1) {
+        VERIFY (m_util.str.is_unit(rs[0], u));
+        digit = m_sk.mk_digit2int(u);
+        propagate_lit(dep, 0, nullptr, mk_simplified_literal(m_autil.mk_ge(digit, m_autil.mk_int(1))));
+    }
+    return true;
+}
+
 /**
    nth(x,idx) = rhs => 
    x = pre(x, idx) ++ unit(rhs) ++ post(x, idx + 1)
@@ -2630,95 +1155,6 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps)  {
     return true;
 }
 
-bool theory_seq::solve_eqs(unsigned i) {
-    context& ctx = get_context();
-    bool change = false;
-    for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
-        eq const& e = m_eqs[i];
-        if (solve_eq(e.ls(), e.rs(), e.dep(), i)) {
-            if (i + 1 != m_eqs.size()) {
-                eq e1 = m_eqs[m_eqs.size()-1];
-                m_eqs.set(i, e1);
-                --i;
-            }
-            ++m_stats.m_num_reductions;
-            m_eqs.pop_back();
-            change = true;
-        }
-        TRACE("seq_verbose", display_equations(tout););
-    }
-    return change || m_new_propagation || ctx.inconsistent();
-}
-
-bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps, unsigned idx) {
-    context& ctx = get_context();
-    expr_ref_vector& ls = m_ls;
-    expr_ref_vector& rs = m_rs;
-    rs.reset(); ls.reset();
-    dependency* dep2 = nullptr;
-    bool change = false;
-    if (!canonize(l, ls, dep2, change)) return false;
-    if (!canonize(r, rs, dep2, change)) return false;
-    deps = m_dm.mk_join(dep2, deps);
-    TRACE("seq_verbose", tout << l << " = " << r << " ==> ";
-          tout << ls << " = " << rs << "\n";
-          display_deps(tout, deps);
-          );
-    if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
-        TRACE("seq", tout << "simplified\n";);
-        return true;
-    }
-    if (!ctx.inconsistent() && lift_ite(ls, rs, deps)) {
-        return true;
-    }
-    TRACE("seq_verbose", tout << ls << " = " << rs << "\n";);
-    if (ls.empty() && rs.empty()) {
-        return true;
-    }
-    if (!ctx.inconsistent() && solve_unit_eq(ls, rs, deps)) {
-        TRACE("seq", tout << "unit\n";);
-        return true;
-    }
-    if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) {
-        TRACE("seq", tout << "binary\n";);
-        return true;
-    }
-    if (!ctx.inconsistent() && solve_nth_eq1(ls, rs, deps)) {
-        return true;
-    }
-    if (!ctx.inconsistent() && solve_nth_eq1(rs, ls, deps)) {
-        return true;
-    }
-    if (!ctx.inconsistent() && solve_itos(rs, ls, deps)) {
-        return true;
-    }
-    if (!ctx.inconsistent() && change) {
-        // The propagation step from arithmetic state (e.g. length offset) to length constraints
-        if (get_context().get_scope_level() == 0) {
-            prop_arith_to_len_offset();
-        }
-        TRACE("seq", tout << "inserting equality\n";);
-        bool updated = false;
-        if (!m_len_offset.empty()) {
-            // Find a better equivalent term for lhs of an equation based on length constraints
-            expr_ref_vector new_ls(m);
-            if (find_better_rep(ls, rs, idx, deps, new_ls)) {
-                eq const & new_eq = eq(m_eq_id++, new_ls, rs, deps);
-                m_eqs.push_back(new_eq);
-                TRACE("seq", tout << "find_better_rep\n";);
-                TRACE("seq", display_equation(tout, new_eq););
-                updated = true;
-            }
-        }
-        if (!updated) {
-            m_eqs.push_back(eq(m_eq_id++, ls, rs, deps));
-        }
-        TRACE("seq", tout << "simplified\n";);
-        return true;
-    }
-    return false;
-}
-
 bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
     unsigned idx;
     expr* s;
@@ -2726,7 +1162,7 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
         std::swap(l, r);
     }
     rational hi;
-    if (m_sk.is_tail(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) {
+    if (m_sk.is_tail_u(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) {
         propagate_lit(deps, 0, nullptr, mk_literal(m_autil.mk_le(mk_len(s), m_autil.mk_int(idx+1))));
         return true;
     }
@@ -3121,7 +1557,7 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
             return true;
         }
     }
-    else if (m_sk.is_tail_match(e, s, l)) {
+    else if (m_sk.is_tail(e, s, l)) {
         // e = tail(s, l), len(s) > l => len(tail(s, l)) = len(s) - l - 1
         // e = tail(s, l), len(s) <= l => len(tail(s, l)) = 0
 
@@ -3151,31 +1587,70 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
 
 
 bool theory_seq::branch_nqs() {
-   if (m_nqs.empty()) {
-       return false;
+   for (unsigned i = 0; i < m_nqs.size(); ++i) {
+       ne n = m_nqs[i];
+       lbool r = branch_nq(n);
+       switch (r) {
+       case l_undef: // needs assignment to a literal.
+           return true;
+       case l_true:  // disequality is satisfied.
+           break;
+       case l_false: // needs to be expanded.
+           if (m_nqs.size() > 1) {
+               ne n2 = m_nqs[m_nqs.size() - 1];
+               m_nqs.set(0, n2);
+           }
+           m_nqs.pop_back();           
+           return true;
+       }
    }
-   ne n = m_nqs[0];
-   branch_nq(n);
-   if (m_nqs.size() > 1) {
-       ne n2 = m_nqs[m_nqs.size() - 1];
-       m_nqs.set(0, n2);
-   }
-   m_nqs.pop_back();
-   return true;
+   return false;
 }
 
-void theory_seq::branch_nq(ne const& n) {
-    literal eq = mk_eq(n.l(), n.r(), false);
+lbool theory_seq::branch_nq(ne const& n) {
+    context& ctx = get_context();
     literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false);
+    ctx.mark_as_relevant(eq_len);
+    switch (ctx.get_assignment(eq_len)) {
+    case l_false:
+        TRACE("seq", ctx.display_literal_smt2(tout << "lengths are different: ", eq_len) << "\n";);
+        return l_true;
+    case l_undef:
+        return l_undef;
+    default:
+        break;
+    }
+    literal eq = mk_eq(n.l(), n.r(), false);
     literal len_gt = mk_literal(m_autil.mk_ge(mk_len(n.l()), m_autil.mk_int(1)));
+    ctx.mark_as_relevant(len_gt);
+    switch (ctx.get_assignment(len_gt)) {
+    case l_false:
+        add_axiom(eq, ~eq_len, len_gt);
+        return l_false;
+    case l_undef:
+        return l_undef;
+    default:
+        break;
+    }
     expr_ref h1(m), t1(m), h2(m), t2(m);
     mk_decompose(n.l(), h1, t1);
     mk_decompose(n.r(), h2, t2);
-
+    literal eq_head = mk_eq(h1, h2, false);
+    ctx.mark_as_relevant(eq_head);
+    switch (ctx.get_assignment(eq_head)) {
+    case l_false:
+        TRACE("seq", ctx.display_literal_smt2(tout << "heads are different: ", eq_head) << "\n";);
+        return l_true;
+    case l_undef:
+        return l_undef;
+    default:
+        break;
+    }
     // l = r or |l| != |r| or |l| > 0
     // l = r or |l| != |r| or h1 != h2 or t1 != t2
     add_axiom(eq, ~eq_len, len_gt);
-    add_axiom(eq, ~eq_len, ~mk_eq(h1, h2, false), ~mk_eq(t1, t2, false));
+    add_axiom(eq, ~eq_len, ~eq_head, ~mk_eq(t1, t2, false));
+    return l_false;
 }
 
 bool theory_seq::solve_nqs(unsigned i) {
@@ -3638,7 +2113,7 @@ bool theory_seq::internalize_term(app* term) {
 
 void theory_seq::add_length(expr* e, expr* l) {
     TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";);
-    SASSERT(!m_length.contains(l));
+    SASSERT(!m_has_length.contains(l));
     m_length.push_back(l);
     m_has_length.insert(e);
     m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_has_length, e));
@@ -3647,7 +2122,6 @@ void theory_seq::add_length(expr* e, expr* l) {
 
 /**
    Add length limit restrictions to sequence s.
-   
  */
 void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
     expr_ref lim_e = m_ax.add_length_limit(s, k);
@@ -3663,9 +2137,8 @@ void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
     if (k0 != 0) {
         m_trail_stack.push(remove_obj_map<theory_seq, expr, unsigned>(m_length_limit_map, s, k0));
     }
-    // std::cout << mk_pp(s, m) << " <= " << k << "\n";
     m_trail_stack.push(insert_obj_map<theory_seq, expr, unsigned>(m_length_limit_map, s));
-    if (is_searching && !get_context().at_base_level()) {
+    if (is_searching) {
         expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth);
         add_axiom(~mk_literal(dlimit), mk_literal(lim_e));
     }
@@ -3693,7 +2166,6 @@ bool theory_seq::add_length_to_eqc(expr* e) {
     return change;
 }
 
-
 void theory_seq::add_int_string(expr* e) {
     m_int_string.push_back(e);
     m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_int_string));
@@ -3702,55 +2174,23 @@ void theory_seq::add_int_string(expr* e) {
 bool theory_seq::check_int_string() {
     bool change = false;
     for (expr * e : m_int_string) {
-        if (check_int_string(e)) {
+        if (check_int_string(e))
             change = true;
-        }
     }
     return change;
 }
 
 bool theory_seq::check_int_string(expr* e) {
-    return 
-        get_context().inconsistent() ||
-        (m_util.str.is_itos(e) && add_itos_val_axiom(e)) ||
-        (m_util.str.is_stoi(e) && add_stoi_val_axiom(e));
-}
-    
-bool theory_seq::add_itos_val_axiom(expr* e) {
     expr* n = nullptr;
-    TRACE("seq", tout << mk_pp(e, m) << "\n";);
-    VERIFY(m_util.str.is_itos(e, n));
-    if (m_util.str.is_stoi(n)) {
-        return false;
-    }
-    add_length_to_eqc(e);
-    return add_si_axiom(e, n);
-}
-
-bool theory_seq::add_stoi_val_axiom(expr* e) {
-    expr* n = nullptr;
-    VERIFY(m_util.str.is_stoi(e, n));    
-    TRACE("seq", tout << mk_pp(e, m) << "\n";);
-    if (m_util.str.is_itos(n)) {
-        return false;
-    }
-    add_length_to_eqc(n);
-    return add_si_axiom(n, e);
-}
-
-bool theory_seq::add_si_axiom(expr* e, expr* n) {
-    rational val1;
-    unsigned val2 = UINT_MAX;
-    if (get_length(e, val1) && val1.is_pos() && val1.is_unsigned() && 
-        (!m_si_axioms.find(e, val2) || val1.get_unsigned() != val2)) {
-        m_ax.add_si_axiom(e, n, val1.get_unsigned());
-        m_si_axioms.insert(e, val1.get_unsigned());
-        m_trail_stack.push(push_replay(alloc(replay_is_axiom, m, e)));
-        m_trail_stack.push(insert_map<theory_seq, obj_map<expr, unsigned>, expr*>(m_si_axioms, e));
+    if (get_context().inconsistent())
+        return true;
+    if (m_util.str.is_itos(e, n) && !m_util.str.is_stoi(n) && add_length_to_eqc(e))
+        return true;
+    if (m_util.str.is_stoi(e, n) && !m_util.str.is_itos(n) && add_length_to_eqc(n))
         return true;
-    }
     return false;
 }
+    
 
 void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
     mk_var(n);
@@ -4265,7 +2705,7 @@ expr_ref theory_seq::elim_skolem(expr* e) {
             todo.pop_back();            
             continue;
         }
-        if (m_sk.is_tail_match(a, x, y) && cache.contains(x) && cache.contains(y)) {
+        if (m_sk.is_tail(a, x, y) && cache.contains(x) && cache.contains(y)) {
             x = cache[x];
             y = cache[y];
             expr_ref y1(m_autil.mk_add(y, m_autil.mk_int(1)), m);
@@ -4653,6 +3093,7 @@ void theory_seq::deque_axiom(expr* n) {
     }
     else if (m_util.str.is_stoi(n)) {
         m_ax.add_stoi_axiom(n);
+        add_length_limit(n, m_max_unfolding_depth, true);
     }
     else if (m_util.str.is_lt(n)) {
         m_ax.add_lt_axiom(n);
@@ -4705,9 +3146,6 @@ void theory_seq::add_length_axiom(expr* n) {
         SASSERT(n != len);
         add_axiom(mk_eq(len, n, false));
     }
-    else if (m_util.str.is_itos(x)) {
-        add_itos_length_axiom(n);
-    }   
     else {
         add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
     }
@@ -4716,62 +3154,6 @@ void theory_seq::add_length_axiom(expr* n) {
     }
 }
 
-void theory_seq::add_itos_length_axiom(expr* len) {
-    expr* x = nullptr, *n = nullptr;
-    VERIFY(m_util.str.is_length(len, x));
-    VERIFY(m_util.str.is_itos(x, n));
-
-    unsigned num_char1 = 1, num_char2 = 1;
-    rational len1, len2;
-    rational ten(10);
-    if (get_num_value(n, len1)) {
-        if (len1.is_neg()) {
-            return;
-        }
-        // 0 <= x < 10
-        // 10 <= x < 100
-        // 100 <= x < 1000
-        rational upper(10);
-        while (len1 > upper) {
-            ++num_char1;
-            upper *= ten;
-        }
-        SASSERT(len1 <= upper);
-    }
-    if (get_num_value(len, len2) && len2.is_unsigned()) {
-        num_char2 = len2.get_unsigned();
-    }
-    unsigned num_char = std::max(num_char1, num_char2);
-
-    add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0))));    
-    literal len_le(mk_literal(m_autil.mk_le(len, m_autil.mk_int(num_char))));
-    literal len_ge(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(num_char))));
-    literal n_ge_0(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
-    add_axiom(~n_ge_0, mk_literal(m_autil.mk_ge(len, m_autil.mk_int(1))));   
-
-    if (num_char == 1) {
-        literal n_ge_10(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(10))));
-        add_axiom(~n_ge_0, n_ge_10, len_le);
-        add_axiom(~len_le, ~n_ge_10);
-        return;
-    }
-    rational hi(1);
-    for (unsigned i = 2; i < num_char; ++i) {
-        hi *= ten;
-    }
-    // n >= hi*10  <=>  len >= num_chars
-    //  n < 100*hi    <=>  len <= num_chars
-    literal n_ge_10hi  = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*hi, true)));
-    literal n_ge_100hi = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*ten*hi, true)));
-    
-    add_axiom(~n_ge_10hi, len_ge);
-    add_axiom(n_ge_10hi, ~len_ge);
-
-    add_axiom(n_ge_100hi, len_le);
-    add_axiom(~n_ge_100hi, ~len_le);
-}
-
-
 
 void theory_seq::propagate_in_re(expr* n, bool is_true) {
     TRACE("seq", tout << mk_pp(n, m) << " <- " << (is_true?"true":"false") << "\n";);
@@ -5252,6 +3634,11 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (m_sk.is_max_unfolding(e)) {
         // no-op
     }
+    else if (m_sk.is_length_limit(e)) {
+        if (is_true) {
+            propagate_length_limit(e);
+        }
+    }
     else if (m_util.str.is_lt(e) || m_util.str.is_le(e)) {
         m_lts.push_back(e);
     }
@@ -5427,13 +3814,11 @@ void theory_seq::relevant_eh(app* n) {
         add_int_string(n);
     }
 
-    expr* s;
-    unsigned idx;
-    if (m_sk.is_tail(n, s, idx)) {
-        add_length_limit(s, m_max_unfolding_depth, true);
+    expr* arg = nullptr;
+    if (m_sk.is_tail(n, arg)) {
+        add_length_limit(arg, m_max_unfolding_depth, true);
     }
 
-    expr* arg;
     if (m_util.str.is_length(n, arg) && !has_length(arg) && get_context().e_internalized(arg)) {
         add_length_to_eqc(arg);
     }
@@ -5480,8 +3865,6 @@ bool theory_seq::is_accept(expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i
     }
 }
 
-
-
 /**
    step(s, idx, re, i, j, t) -> nth(s, idx) == t & len(s) > idx
    step(s, idx, re, i, j, t) -> accept(s, idx + 1, re, j)
@@ -5608,8 +3991,8 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
     }
     if (k_min < UINT_MAX) {
         m_max_unfolding_depth++;
-        IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << k_min << ")\n");
-        add_length_limit(s, 2*k_min, false);
+        IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_pp(s_min, m) << " " << 2*k_min << ")\n");
+        add_length_limit(s_min, 2*k_min, false);
         return true;
     }
     else if (has_max_unfolding) {
@@ -5621,6 +4004,18 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
 }
 
 
+void theory_seq::propagate_length_limit(expr* e) {
+    unsigned k = 0;
+    expr* s = nullptr, *i = nullptr;
+    VERIFY(m_sk.is_length_limit(e, k, s));
+    if (m_util.str.is_stoi(s)) {
+        m_ax.add_stoi_axiom(s, k);
+    }    
+    if (m_util.str.is_itos(s)) {
+        m_ax.add_itos_axiom(s, k);
+    }
+}
+
 /*
   !prefix(e1,e2) => e1 != ""
   !prefix(e1,e2) => len(e1) > len(e2) or e1 = xcy & e2 = xdz & c != d
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 81d78bd5f..d1c181799 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -389,13 +389,12 @@ namespace smt {
         obj_hashtable<expr>        m_axiom_set;
         unsigned                   m_axioms_head; // index of first axiom to add.
         bool                       m_incomplete;             // is the solver (clearly) incomplete for the fragment.
-        expr_ref_vector     m_int_string;
-        obj_map<expr, unsigned> m_si_axioms;
-        obj_hashtable<expr> m_has_length;         // is length applied
-        expr_ref_vector     m_length;             // length applications themselves
-        obj_map<expr, unsigned> m_length_limit_map;   // sequences that have length limit predicates
-        expr_ref_vector         m_length_limit;       // length limit predicates
-        scoped_ptr_vector<apply> m_replay;        // set of actions to replay
+        expr_ref_vector            m_int_string;
+        obj_hashtable<expr>        m_has_length;         // is length applied
+        expr_ref_vector            m_length;             // length applications themselves
+        obj_map<expr, unsigned>    m_length_limit_map;   // sequences that have length limit predicates
+        expr_ref_vector            m_length_limit;       // length limit predicates
+        scoped_ptr_vector<apply>   m_replay;        // set of actions to replay
         model_generator* m_mg;
         th_rewriter      m_rewrite;               // rewriter that converts strings to character concats
         th_rewriter      m_str_rewrite;           // rewriter that coonverts character concats to strings
@@ -518,6 +517,7 @@ namespace smt {
         bool solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         bool solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         bool solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
+        bool solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep);
         bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr_ref& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr_ref& y);
         bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
         bool is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1);
@@ -541,7 +541,7 @@ namespace smt {
         bool solve_ne(unsigned i);
         bool solve_nc(unsigned i);
         bool branch_nqs();
-        void branch_nq(ne const& n);
+        lbool branch_nq(ne const& n);
 
         struct cell {
             cell*       m_parent;
@@ -622,10 +622,6 @@ namespace smt {
 
         expr_ref add_elim_string_axiom(expr* n);
         void add_in_re_axiom(expr* n);
-        bool add_itos_val_axiom(expr* n);
-        bool add_stoi_val_axiom(expr* n);
-        bool add_si_axiom(expr* e, expr* n);
-        void add_itos_length_axiom(expr* n);
         literal mk_literal(expr* n);
         literal mk_simplified_literal(expr* n);
         literal mk_eq_empty(expr* n, bool phase = true);
@@ -650,6 +646,9 @@ namespace smt {
 
         void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
 
+        // unfold definitions based on length limits
+        void propagate_length_limit(expr* n);
+
         void set_incomplete(app* term);
 
         // automata utilities
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index ac4a37750..de04dfc0c 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -19,9 +19,10 @@ Revision History:
 #ifndef THEORY_SEQ_EMPTY_H_
 #define THEORY_SEQ_EMPTY_H_
 
-#include "smt/smt_theory.h"
 #include "ast/seq_decl_plugin.h"
 #include "model/seq_factory.h"
+#include "smt/smt_theory.h"
+#include "smt/smt_model_generator.h"
 
 namespace smt {