diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h
index 1b3101e15..d124dd39f 100644
--- a/src/ast/rewriter/seq_axioms.h
+++ b/src/ast/rewriter/seq_axioms.h
@@ -111,6 +111,9 @@ namespace seq {
         expr_ref mk_ge(expr* x, rational const& n) { return mk_ge_e(x, a.mk_int(n)); }
         expr_ref mk_le(expr* x, rational const& n) { return mk_le_e(x, a.mk_int(n)); }
 
+        void rewrite(expr_ref& e) { m_rewrite(e); }
+        skolem& sk() { return m_sk; }
+
     };
 
 };
diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp
index 404e31307..a268f3c41 100644
--- a/src/ast/rewriter/seq_eq_solver.cpp
+++ b/src/ast/rewriter/seq_eq_solver.cpp
@@ -8,7 +8,7 @@ Module Name:
 Abstract:
 
     Solver-agnostic equality solving routines for sequences
-    
+
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-01
@@ -35,9 +35,25 @@ namespace seq {
             return true;
         if (reduce_itos2(e, r))
             return true;
+        if (reduce_itos3(e, r))
+            return true;
         if (reduce_binary_eq(e, r))
             return true;
-        
+        if (reduce_nth_solved(e, r))
+            return true;
+
+        return false;
+    }
+
+
+    bool eq_solver::branch(unsigned priority, eqr const& e) {
+        switch (priority) {
+        case 0:
+            return branch_unit_variable(e);
+        case 1:
+        default:
+            break;
+        }
         return false;
     }
 
@@ -64,15 +80,15 @@ namespace seq {
      * --------------------------
      * s = t or (s < 0 and t < 0)
      */
-        
+
     bool eq_solver::match_itos1(eqr const& e, expr*& a, expr*& b) {
-        return 
-            e.ls.size() == 1 && e.rs.size() == 1 && 
+        return
+            e.ls.size() == 1 && e.rs.size() == 1 &&
             seq.str.is_itos(e.ls[0], a) && seq.str.is_itos(e.rs[0], b);
     }
 
     bool eq_solver::reduce_itos1(eqr const& e, eq_ptr& r) {
-        expr* s = nullptr, *t = nullptr;
+        expr* s = nullptr, * t = nullptr;
         if (!match_itos1(e, s, t))
             return false;
         expr_ref eq = mk_eq(s, t);
@@ -86,7 +102,7 @@ namespace seq {
      * -----------------
      *       s < 0
      */
-    
+
     bool eq_solver::match_itos2(eqr const& e, expr*& s) {
         if (e.ls.size() == 1 && e.rs.empty() && seq.str.is_itos(e.ls[0], s))
             return true;
@@ -103,11 +119,78 @@ namespace seq {
         return true;
     }
 
+    /**
+    *       itos(n) = ""
+    *       ------------
+    *          n <= -1
+    *
+    *          itos(n) = [d1]+[d2]+...+[dk]
+    *       ---------------------------------
+    *           n = 10^{k-1}*d1 + ... + dk
+    *
+    *           k > 1 => d1 > 0
+    */
+
+    bool eq_solver::match_itos3(eqr const& e, expr*& n, expr_ref_vector const*& es) {
+        if (e.ls.size() == 1 && seq.str.is_itos(e.ls[0], n)) {
+            es = &e.rs;
+            return true;
+        }
+        if (e.rs.size() == 1 && seq.str.is_itos(e.rs[0], n)) {
+            es = &e.ls;
+            return true;
+        }
+        return false;
+    }
+
+    bool eq_solver::reduce_itos3(eqr const& e, eq_ptr& r) {
+        expr* n = nullptr;
+        expr_ref_vector const* _es = nullptr;
+        if (!match_itos3(e, n, _es))
+            return false;
+        expr_ref_vector const& es = *_es;
+
+        if (es.empty()) {
+            add_consequence(m_ax.mk_le(n, -1));
+            return true;
+        }
+        expr* u = nullptr;
+        for (expr* r : es) {
+            if (seq.str.is_unit(r, u)) {
+                expr_ref is_digit = m_ax.is_digit(u);
+                if (!m.is_true(ctx.expr2rep(is_digit)))
+                    add_consequence(is_digit);
+            }
+        }
+        if (!all_units(es, 0, es.size()))
+            return false;
+
+        expr_ref num(m);
+        for (expr* r : es) {
+            VERIFY(seq.str.is_unit(r, u));
+            expr_ref digit = m_ax.sk().mk_digit2int(u);
+            if (!num)
+                num = digit;
+            else
+                num = a.mk_add(a.mk_mul(a.mk_int(10), num), digit);
+        }
+
+        expr_ref eq(m.mk_eq(n, num), m);
+        m_ax.rewrite(eq);
+        add_consequence(eq);
+        if (es.size() > 1) {
+            VERIFY(seq.str.is_unit(es[0], u));
+            expr_ref digit = m_ax.sk().mk_digit2int(u);
+            add_consequence(m_ax.mk_ge(digit, 1));
+        }
+        return true;
+    }
+
     /**
      *    x = t, where x does not occur in t.
      */
     bool eq_solver::reduce_unit(eqr const& e, eq_ptr& r) {
-        if (e.ls == e.rs) 
+        if (e.ls == e.rs)
             return true;
         if (e.ls.size() == 1 && is_var(e.ls[0]) && !occurs(e.ls[0], e.rs)) {
             expr_ref y(seq.str.mk_concat(e.rs, e.ls[0]->get_sort()), m);
@@ -145,7 +228,7 @@ namespace seq {
             set_conflict();
             return true;
         }
-        if (xs.empty()) 
+        if (xs.empty())
             return true;
 
         if (xs.size() != 1)
@@ -155,29 +238,105 @@ namespace seq {
             return false;
         expr_ref eq(m.mk_eq(xs[0], ys[0]), m);
         expr* veq = ctx.expr2rep(eq);
-        if (m.is_true(veq)) 
+        if (m.is_true(veq))
             return false;
         add_consequence(eq);
         return m.is_false(veq);
     }
 
+    /**
+    *   x = nth(unit(x, 0)) ++ ... ++ nth(unit(x,i))
+    * ------------------------------------------------
+    *   x -> nth(unit(x, 0)) ++ ... ++ nth(unit(x,i))
+    */
+
+    bool eq_solver::reduce_nth_solved(eqr const& e, eq_ptr& r) {
+        expr_ref x(m), y(m);
+        if (match_nth_solved(e, x, y)) {
+            ctx.add_solution(x, y);
+            return true;
+        }
+        return false;
+    }
+
+    bool eq_solver::match_nth_solved(eqr const& e, expr_ref& x, expr_ref& y) {
+        if (match_nth_solved_aux(e.ls, e.rs, x, y))
+            return true;
+        if (match_nth_solved_aux(e.rs, e.ls, x, y))
+            return true;
+        return false;
+    }
+
+    bool eq_solver::match_nth_solved_aux(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, expr_ref& y) {
+        if (ls.size() != 1 || !is_var(ls[0]))
+            return false;
+        expr* n = nullptr, * u = nullptr;
+        unsigned j = 0, i = 0;
+        for (expr* r : rs) {
+            if (seq.str.is_unit(r, u) && seq.str.is_nth_i(u, n, i) && i == j && n == ls[0])
+                ++j;
+            else
+                return false;
+        }
+        x = ls[0];
+        y = seq.str.mk_concat(rs, x->get_sort());
+        return true;
+    }
+
+    /**
+    *  XV == abcdef, where V is an arbitrary string
+    * ---------------------------------------------
+    *          |X| <= |abcdef|
+    * 
+    *     |X| = k => X = a_1...a_k
+    */
+
+    bool eq_solver::branch_unit_variable(expr* X, expr_ref_vector const& units) {
+        SASSERT(is_var(X));
+        rational lenX;
+        ctx.get_length(X, lenX);
+
+        if (lenX > units.size()) {
+            add_consequence(m_ax.mk_le(seq.str.mk_length(X), units.size()));
+            return true;
+        }
+
+        expr_ref eq_length(m.mk_eq(a.mk_int(lenX), seq.str.mk_length(X)), m);
+        expr* val = ctx.expr2rep(eq_length);
+        if (!m.is_false(val)) {
+            expr_ref Y(seq.str.mk_concat(lenX.get_unsigned(), units.c_ptr(), X->get_sort()), m);
+            expr_ref eq = m_ax.sk().mk_eq(X, Y);
+            add_consequence(~eq_length, eq);
+            return true;
+        }     
+        return false;
+    }
+
+    bool eq_solver::branch_unit_variable(eqr const& e) {
+        if (!e.ls.empty() && is_var(e.ls[0]) && all_units(e.rs, 0, e.rs.size()))
+            return branch_unit_variable(e.ls[0], e.rs);
+        if (!e.rs.empty() && is_var(e.rs[0]) && all_units(e.ls, 0, e.ls.size()))
+            return branch_unit_variable(e.rs[0], e.ls);
+        return false;
+    }
+
 
     bool eq_solver::is_var(expr* a) const {
         return
             seq.is_seq(a) &&
             !seq.str.is_concat(a) &&
-            !seq.str.is_empty(a)  &&
+            !seq.str.is_empty(a) &&
             !seq.str.is_string(a) &&
             !seq.str.is_unit(a) &&
             !seq.str.is_itos(a) &&
-            !seq.str.is_nth_i(a) && 
+            !seq.str.is_nth_i(a) &&
             !m.is_ite(a);
     }
 
     bool eq_solver::occurs(expr* a, expr_ref_vector const& b) {
-        for (auto const& elem : b) 
-            if (a == elem || m.is_ite(elem)) 
-                return true;        
+        for (auto const& elem : b)
+            if (a == elem || m.is_ite(elem))
+                return true;
         return false;
     }
 
@@ -185,7 +344,7 @@ namespace seq {
         // true if a occurs under an interpreted function or under left/right selector.
         SASSERT(is_var(a));
         SASSERT(m_todo.empty());
-        expr* e1 = nullptr, *e2 = nullptr;
+        expr* e1 = nullptr, * e2 = nullptr;
         m_todo.push_back(b);
         while (!m_todo.empty()) {
             b = m_todo.back();
@@ -220,8 +379,8 @@ namespace seq {
 
     unsigned eq_solver::count_units_l2r(expr_ref_vector const& es, unsigned offset) const {
         unsigned i = offset, sz = es.size();
-        for (; i < sz && seq.str.is_unit(es[i]); ++i) ;
-        return i - offset;                        
+        for (; i < sz && seq.str.is_unit(es[i]); ++i);
+        return i - offset;
     }
 
     unsigned eq_solver::count_units_r2l(expr_ref_vector const& es, unsigned offset) const {
@@ -231,15 +390,14 @@ namespace seq {
             if (!seq.str.is_unit(es[i]))
                 break;
             ++count;
-        }
-        while (i-- > 0);
+        } while (i-- > 0);
         return count;
     }
 
     unsigned eq_solver::count_non_units_l2r(expr_ref_vector const& es, unsigned offset) const {
         unsigned i = offset, sz = es.size();
-        for (; i < sz && !seq.str.is_unit(es[i]); ++i) ;
-        return i - offset;                        
+        for (; i < sz && !seq.str.is_unit(es[i]); ++i);
+        return i - offset;
     }
 
     unsigned eq_solver::count_non_units_r2l(expr_ref_vector const& es, unsigned offset) const {
@@ -249,8 +407,7 @@ namespace seq {
             if (seq.str.is_unit(es[i]))
                 break;
             ++count;
-        }
-        while (i-- > 0);
+        } while (i-- > 0);
         return count;
     }
 
@@ -259,9 +416,9 @@ namespace seq {
      * where U is a variable or concatenation of variables
      */
 
-    bool eq_solver::match_ternary_eq_r(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) {
-        if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {            
+    bool eq_solver::match_ternary_eq_r(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) {
+        if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
             unsigned num_ls_units = count_units_r2l(ls, ls.size() - 1);
             if (num_ls_units == 0 || num_ls_units == ls.size())
                 return false;
@@ -273,33 +430,33 @@ namespace seq {
             unsigned num_rs_units = count_units_r2l(rs, rs.size() - 1 - num_rs_non_units);
             if (num_rs_units == 0)
                 return false;
-            set_prefix(x,   ls, ls.size() - num_ls_units);
-            set_suffix(xs,  ls, num_ls_units);
+            set_prefix(x, ls, ls.size() - num_ls_units);
+            set_suffix(xs, ls, num_ls_units);
             unsigned offset = rs.size() - num_rs_non_units - num_rs_units;
-            set_prefix(y1,  rs, offset);
+            set_prefix(y1, rs, offset);
             set_extract(ys, rs, offset, num_rs_units);
-            set_suffix(y2,  rs, num_rs_non_units);
+            set_suffix(y2, rs, num_rs_non_units);
             return true;
         }
         return false;
     }
 
-    bool eq_solver::match_ternary_eq_rhs(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 eq_solver::match_ternary_eq_rhs(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) {
         if (match_ternary_eq_r(ls, rs, x, xs, y1, ys, y2))
             return true;
         if (match_ternary_eq_r(rs, ls, x, xs, y1, ys, y2))
             return true;
         return false;
     }
-    
+
     /*
       match: abc X ..  = Y def Z ..
          where Y is a variable or concatenation of variables
     */
 
-    bool eq_solver::match_ternary_eq_l(expr_ref_vector const& ls, expr_ref_vector const& rs, 
-                                       expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
+    bool eq_solver::match_ternary_eq_l(expr_ref_vector const& ls, expr_ref_vector const& rs,
+        expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
         if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
             unsigned num_ls_units = count_units_l2r(ls, 0);
             if (num_ls_units == 0 || num_ls_units == ls.size())
@@ -310,18 +467,18 @@ namespace seq {
             unsigned num_rs_units = count_units_l2r(rs, num_rs_non_units);
             if (num_rs_units == 0)
                 return false;
-            set_prefix(xs,  ls, num_ls_units);
-            set_suffix(x,   ls, ls.size() - num_ls_units);
-            set_prefix(y1,  rs, num_rs_non_units);
+            set_prefix(xs, ls, num_ls_units);
+            set_suffix(x, ls, ls.size() - num_ls_units);
+            set_prefix(y1, rs, num_rs_non_units);
             set_extract(ys, rs, num_rs_non_units, num_rs_units);
-            set_suffix(y2,  rs, rs.size() - num_rs_non_units - num_rs_units);
+            set_suffix(y2, rs, rs.size() - num_rs_non_units - num_rs_units);
             return true;
         }
         return false;
     }
 
-    bool eq_solver::match_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs, 
-                                         expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
+    bool eq_solver::match_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs,
+        expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
         if (match_ternary_eq_l(ls, rs, xs, x, y1, ys, y2))
             return true;
         if (match_ternary_eq_l(rs, ls, xs, x, y1, ys, y2))
@@ -331,8 +488,8 @@ namespace seq {
 
 
     bool eq_solver::all_units(expr_ref_vector const& es, unsigned start, unsigned end) const {
-        for (unsigned i = start; i < end; ++i) 
-            if (!seq.str.is_unit(es[i])) 
+        for (unsigned i = start; i < end; ++i)
+            if (!seq.str.is_unit(es[i]))
                 return false;
         return true;
     }
@@ -340,9 +497,9 @@ namespace seq {
     /**
        match X abc = defg Y, for abc, defg non-empty
     */
-    
-    bool eq_solver::match_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
-                                    expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
+
+    bool eq_solver::match_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
+        expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
         if (ls.size() > 1 && is_var(ls[0]) &&
             rs.size() > 1 && is_var(rs.back()) &&
             all_units(ls, 1, ls.size()) &&
@@ -369,8 +526,8 @@ namespace seq {
      */
 
     bool eq_solver::match_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) {
+        expr_ref& x1, expr_ref_vector& xs, expr_ref& x2,
+        expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
         if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
             rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
             unsigned ls_non_unit = count_non_units_l2r(ls, 0);
@@ -385,18 +542,78 @@ namespace seq {
                 return false;
             if (rs_unit == 0)
                 return false;
-            set_prefix(x1,  ls, ls_non_unit);
+            set_prefix(x1, ls, ls_non_unit);
             set_extract(xs, ls, ls_non_unit, ls_unit);
-            set_suffix(x2,  ls, ls.size() - ls_non_unit - ls_unit);
-            set_prefix(y1,  rs, rs_non_unit);
+            set_suffix(x2, ls, ls.size() - ls_non_unit - ls_unit);
+            set_prefix(y1, rs, rs_non_unit);
             set_extract(ys, rs, rs_non_unit, rs_unit);
-            set_suffix(y2,  rs, rs.size() - rs_non_unit - rs_unit);
+            set_suffix(y2, rs, rs.size() - rs_non_unit - rs_unit);
             return true;
         }
         return false;
     }
 
 
+    // exists x, y, rs' != empty s.t.  (ls = x ++ rs ++ y) || (ls = rs' ++ y && rs = x ++ rs')
+    bool eq_solver::can_align_from_lhs_aux(expr_ref_vector const& ls, expr_ref_vector const& rs) {
+        SASSERT(!ls.empty() && !rs.empty());
+
+        for (unsigned i = 0; i < ls.size(); ++i) {
+            if (m.are_distinct(ls[i], rs.back()))
+                continue;
+            
+            if (i == 0)
+                return true;
+            // ls = rs' ++ y && rs = x ++ rs', diff = |x|
+            bool same = true;
+            if (rs.size() > i) {
+                unsigned diff = rs.size() - (i + 1);
+                for (unsigned j = 0; same && j < i; ++j) 
+                    same = !m.are_distinct(ls[j], rs[diff + j]);                               
+            }
+            // ls = x ++ rs ++ y, diff = |x|
+            else {
+                unsigned diff = (i + 1) - rs.size();
+                for (unsigned j = 0; same && j + 1 < rs.size(); ++j) 
+                    same = !m.are_distinct(ls[diff + j], rs[j]);                              
+            }
+            if (same)
+                return true;
+        }
+        return false;
+    }
+
+    // exists x, y, rs' != empty s.t.  (ls = x ++ rs ++ y) || (ls = x ++ rs' && rs = rs' ++ y)
+    bool eq_solver::can_align_from_rhs_aux(expr_ref_vector const& ls, expr_ref_vector const& rs) {
+        SASSERT(!ls.empty() && !rs.empty());
+
+        for (unsigned i = 0; i < ls.size(); ++i) {
+            unsigned diff = ls.size() - 1 - i;
+            if (m.are_distinct(ls[diff], rs[0]))
+                continue;
+            
+            if (i == 0) 
+                return true;
+            
+            bool same = true;
+            // ls = x ++ rs' && rs = rs' ++ y, diff = |x|
+            if (rs.size() > i) {
+                for (unsigned j = 1; same && j <= i; ++j) 
+                    same = !m.are_distinct(ls[diff + j], rs[j]);                
+            }
+            // ls = x ++ rs ++ y, diff = |x|
+            else {
+                for (unsigned j = 1; same && j < rs.size(); ++j)
+                    same = !m.are_distinct(ls[diff + j], rs[j]);
+            }
+            if (same)
+                return true;
+        }
+        return false;
+    }
+
+
+
 
 };
 
diff --git a/src/ast/rewriter/seq_eq_solver.h b/src/ast/rewriter/seq_eq_solver.h
index 3183d8418..1053b143d 100644
--- a/src/ast/rewriter/seq_eq_solver.h
+++ b/src/ast/rewriter/seq_eq_solver.h
@@ -16,6 +16,7 @@ Author:
 --*/
 #pragma once
 
+#include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/seq_axioms.h"
 
 namespace seq {
@@ -48,6 +49,7 @@ namespace seq {
         ast_manager&       m;
         eq_solver_context& ctx;
         axioms&            m_ax;
+        arith_util         a;
         seq_util           seq;
         expr_ref_vector    m_clause;
 
@@ -59,9 +61,16 @@ namespace seq {
         bool match_itos2(eqr const& e, expr*& s);
         bool reduce_itos2(eqr const& e, eq_ptr& r);
 
+        bool reduce_itos3(eqr const& e, eq_ptr& r);
+        bool match_itos3(eqr const& e, expr*& n, expr_ref_vector const* & es);
+
         bool match_binary_eq(eqr const& e, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y);
         bool reduce_binary_eq(eqr const& e, eq_ptr& r);
 
+        bool reduce_nth_solved(eqr const& e, eq_ptr& r);
+        bool match_nth_solved(eqr const& e, expr_ref& x, expr_ref& y);
+        bool match_nth_solved_aux(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, expr_ref& y);
+
         bool match_ternary_eq_r(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);
 
@@ -69,6 +78,10 @@ namespace seq {
                                 expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
 
 
+        bool branch_unit_variable(eqr const& e);
+        bool branch_unit_variable(expr* X, expr_ref_vector const& units);
+
+
         /**
          * count unit or non-unit entries left-to-right or right-to-left starting at, and including offset.
          */
@@ -115,6 +128,7 @@ namespace seq {
             m(m),
             ctx(ctx),
             m_ax(ax),
+            a(m),
             seq(m),
             m_clause(m)
         {}
@@ -123,6 +137,8 @@ namespace seq {
 
         bool reduce(expr* s, expr* t, eq_ptr& r);
 
+        bool branch(unsigned priority, eqr const& e);
+
         bool is_var(expr* a) const;
 
         bool match_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
@@ -137,6 +153,9 @@ namespace seq {
         bool match_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 can_align_from_lhs_aux(expr_ref_vector const& ls, expr_ref_vector const& rs);
+        bool can_align_from_rhs_aux(expr_ref_vector const& ls, expr_ref_vector const& rs);
         
     };
 
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 9c22e0e06..d7b96a902 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -125,6 +125,10 @@ expr * model::get_fresh_value(sort * s) {
     return get_factory(s)->get_fresh_value(s);
 }
 
+void model::register_value(expr* e) {
+    get_factory(e->get_sort())->register_value(e);
+}
+
 bool model::get_some_values(sort * s, expr_ref& v1, expr_ref& v2) {
     return get_factory(s)->get_some_values(s, v1, v2);
 }
diff --git a/src/model/model.h b/src/model/model.h
index cbb0db08a..ea4a38fdd 100644
--- a/src/model/model.h
+++ b/src/model/model.h
@@ -70,6 +70,7 @@ public:
 
     expr * get_some_value(sort * s) override;
     expr * get_fresh_value(sort * s) override;
+    void register_value(expr* n);
     bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override;
 
     ptr_vector<expr> const & get_universe(sort * s) const override;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 6d7dda150..c143988ba 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1029,7 +1029,7 @@ namespace sat {
                     return false;
             } while (m_qhead < m_trail.size());
 
-            if (m_ext) 
+            if (m_ext && !is_probing()) 
                 m_ext->unit_propagate();            
         }
         if (m_inconsistent)
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index e1d99b9d8..2115eb9d3 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -626,12 +626,16 @@ namespace arith {
             ctx.get_rewriter()(value);
         }
         else {
-            UNREACHABLE();
+            value = mdl.get_fresh_value(o->get_sort());
         }
+        mdl.register_value(value);
         values.set(n->get_root_id(), value);
     }
 
-    void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
+    bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
+        theory_var v = n->get_th_var(get_id());
+        if (v == euf::null_theory_var && !a.is_arith_expr(n->get_expr()))
+            return false;
         expr* e = n->get_expr();
         if (a.is_arith_expr(e) && to_app(e)->get_num_args() > 0) {
             for (auto* arg : euf::enode_args(n))
@@ -640,6 +644,7 @@ namespace arith {
         else {
             dep.insert(n, nullptr); 
         }
+        return true;
     }
 
     void solver::push_core() {
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 2191cb029..8659221c9 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -429,7 +429,7 @@ namespace arith {
         void init_model() override;
         void finalize_model(model& mdl) override { DEBUG_CODE(dbg_finalize_model(mdl);); }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
-        void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
+        bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void internalize(expr* e, bool redundant) override;
         void eq_internalized(euf::enode* n) override;
diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index d59e42635..0ca3bb48e 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -22,10 +22,10 @@ Author:
 namespace array {
     
     
-    void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { 
+    bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { 
         if (!a.is_array(n->get_expr())) {
             dep.insert(n, nullptr);
-            return;
+            return true;
         }
         for (euf::enode* p : euf::enode_parents(n)) {
             if (a.is_default(p->get_expr())) {
@@ -41,6 +41,7 @@ namespace array {
         for (euf::enode* k : euf::enode_class(n)) 
             if (a.is_const(k->get_expr()))
                 dep.add(n, k->get_arg(0));    
+        return true;
     }
 
 
diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index 6fef43bec..a039b8dfb 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -207,7 +207,7 @@ namespace array {
         void new_diseq_eh(euf::th_eq const& eq) override;
         bool unit_propagate() override;
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
-        void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
+        bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void internalize(expr* e, bool redundant) override;
         euf::theory_var mk_var(euf::enode* n) override;
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index 387922dab..7e17c001c 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -703,15 +703,16 @@ namespace dt {
         values.set(n->get_root_id(), m.mk_app(c_decl, m_args));
     }
 
-    void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
+    bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
         theory_var v = n->get_th_var(get_id());
         if (!is_datatype(n->get_expr()))
-            return;
+            return true;
         euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
         if (con->num_args() == 0)
             dep.insert(n, nullptr);
         for (enode* arg : euf::enode_args(con))
             dep.add(n, arg->get_root());
+        return true;
     }
 
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h
index 2dd4929d3..7e78acb27 100644
--- a/src/sat/smt/dt_solver.h
+++ b/src/sat/smt/dt_solver.h
@@ -149,7 +149,7 @@ namespace dt {
         void new_eq_eh(euf::th_eq const& eq) override;
         bool unit_propagate() override { return false; }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
-        void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
+        bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         sat::literal internalize(expr* e, bool sign, bool root, bool redundant) override;
         void internalize(expr* e, bool redundant) override;
         euf::theory_var mk_var(euf::enode* n) override;
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 58748c9ca..3695a6036 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -88,18 +88,31 @@ namespace euf {
     }
 
     void solver::collect_dependencies(user_sort& us, deps_t& deps) {
+        ptr_buffer<enode> fresh_values;
         for (enode* n : m_egraph.nodes()) {
             expr* e = n->get_expr();
             sort* srt = e->get_sort();
             auto* mb = sort2solver(srt);
-            if (mb)
-                mb->add_dep(n, deps);
-            else
+            if (!mb) 
                 deps.insert(n, nullptr);
+            else if (!mb->add_dep(n, deps))
+                fresh_values.push_back(n);
             if (n->is_root() && m.is_uninterp(srt) && m.is_value(e))
                 us.register_value(e);
         }
 
+        // fresh values depend on all non-fresh values of the same sort
+        for (enode* n : fresh_values) {
+            n->mark1();
+            deps.insert(n, nullptr);
+        }
+        for (enode* n : fresh_values)
+            for (enode* r : m_egraph.nodes())
+                if (r->is_root() && r->get_sort() == n->get_sort() && !r->is_marked1())
+                    deps.add(n, r);
+        for (enode* n : fresh_values)
+            n->unmark1();
+        
         TRACE("euf",
               for (auto const& d : deps.deps()) 
                   if (d.m_value) {
diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
index 80c4f6e0e..5904376f0 100644
--- a/src/sat/smt/fpa_solver.cpp
+++ b/src/sat/smt/fpa_solver.cpp
@@ -318,22 +318,27 @@ namespace fpa {
         values.set(n->get_root_id(), value);
     }
 
-    void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
+    bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
         expr* e = n->get_expr();
         if (m_fpa_util.is_fp(e)) {
             SASSERT(n->num_args() == 3);
             for (enode* arg : euf::enode_args(n))
                 dep.add(n, arg);
+            return true;
         }
         else if (m_fpa_util.is_bv2rm(e)) {
             SASSERT(n->num_args() == 1);
             dep.add(n, n->get_arg(0));
+            return true;
         }
         else if (m_fpa_util.is_rm(e) || m_fpa_util.is_float(e)) {
             euf::enode* wrapped = expr2enode(m_converter.wrap(e));
             if (wrapped)
                 dep.add(n, wrapped);
+            return nullptr != wrapped;
         }
+        else 
+            return false;
     }
 
     std::ostream& solver::display(std::ostream& out) const {
diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h
index a7e866ccd..9f0d8ae36 100644
--- a/src/sat/smt/fpa_solver.h
+++ b/src/sat/smt/fpa_solver.h
@@ -64,7 +64,7 @@ namespace fpa {
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; }
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
-        void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
+        bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         void finalize_model(model& mdl) override;
 
         bool unit_propagate() override { return false; }
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index 67b15e8e3..3c1c369b9 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -79,7 +79,7 @@ namespace euf {
         /**
            \brief compute dependencies for node n
          */
-        virtual void add_dep(euf::enode* n, top_sort<euf::enode>& dep) { dep.insert(n, nullptr); }
+        virtual bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) { dep.insert(n, nullptr); return true; }
 
         /**
            \brief should function be included in model.
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 715d067a4..5299524c1 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -75,13 +75,10 @@ bool theory_seq::solve_eq(unsigned idx) {
     }
 
     TRACE("seq_verbose", tout << ls << " = " << rs << "\n";);
-    if (!ctx.inconsistent() && solve_nth_eq1(ls, rs, deps)) {
+    if (!ctx.inconsistent() && solve_nth_eq(ls, rs, deps)) {
         return true;
     }
-    if (!ctx.inconsistent() && solve_nth_eq1(rs, ls, deps)) {
-        return true;
-    }
-    if (!ctx.inconsistent() && solve_itos(rs, ls, deps)) {
+    if (!ctx.inconsistent() && solve_nth_eq(rs, ls, deps)) {
         return true;
     }
     if (!ctx.inconsistent() && change) {
@@ -674,42 +671,11 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c
     expr_ref r = mk_concat(rs);
     expr_ref pair(m.mk_eq(l,r), m);
     bool result;
-    if (m_overlap_lhs.find(pair, result)) {
-        return result;
+    if (!m_overlap_lhs.find(pair, result)) {
+        result = m_eq.can_align_from_lhs_aux(ls, rs);
+        m_overlap_lhs.insert(pair, result);
     }
-    for (unsigned i = 0; i < ls.size(); ++i) {
-        if (!m.are_distinct(ls[i], rs.back())) {
-            bool same = true;
-            if (i == 0) {
-                m_overlap_lhs.insert(pair, true);
-                return true;
-            }
-            // ls = rs' ++ y && rs = x ++ rs', diff = |x|
-            if (rs.size() > i) {
-                unsigned diff = rs.size() - (i + 1);
-                for (unsigned j = 0; same && j < i; ++j) {
-                    same = !m.are_distinct(ls[j], rs[diff + j]);
-                }
-                if (same) {
-                    m_overlap_lhs.insert(pair, true);
-                    return true;
-                }
-            }
-            // ls = x ++ rs ++ y, diff = |x|
-            else {
-                unsigned diff = (i + 1) - rs.size();
-                for (unsigned j = 0; same && j + 1 < rs.size(); ++j) {
-                    same = !m.are_distinct(ls[diff + j], rs[j]);
-                }
-                if (same) {
-                    m_overlap_lhs.insert(pair, true);
-                    return true;
-                }
-            }
-        }
-    }
-    m_overlap_lhs.insert(pair, false);
-    return false;
+    return result;
 }
 
 // exists x, y, rs' != empty s.t.  (ls = x ++ rs ++ y) || (ls = x ++ rs' && rs = rs' ++ y)
@@ -717,45 +683,16 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c
     SASSERT(!ls.empty() && !rs.empty());
     expr_ref l = mk_concat(ls);
     expr_ref r = mk_concat(rs);
-    expr_ref pair(m.mk_eq(l,r), m);
+    expr_ref pair(m.mk_eq(l, r), m);
     bool result;
-    if (m_overlap_rhs.find(pair, result)) {
-        return result;
+    if (!m_overlap_rhs.find(pair, result)) {
+        result = m_eq.can_align_from_rhs_aux(ls, rs);
+        m_overlap_rhs.insert(pair, result);
     }
-    for (unsigned i = 0; i < ls.size(); ++i) {
-        unsigned diff = ls.size()-1-i;
-        if (!m.are_distinct(ls[diff], rs[0])) {
-            bool same = true;
-            if (i == 0) {
-                m_overlap_rhs.insert(pair, true);
-                return true;
-            }
-            // ls = x ++ rs' && rs = rs' ++ y, diff = |x|
-            if (rs.size() > i) {
-                for (unsigned j = 1; same && j <= i; ++j) {
-                    same = !m.are_distinct(ls[diff+j], rs[j]);
-                }
-                if (same) {
-                    m_overlap_rhs.insert(pair, true);
-                    return true;
-                }
-            }
-            // ls = x ++ rs ++ y, diff = |x|
-            else {
-                for (unsigned j = 1; same && j < rs.size(); ++j) {
-                    same = !m.are_distinct(ls[diff + j], rs[j]);
-                }
-                if (same) {
-                    m_overlap_rhs.insert(pair, true);
-                    return true;
-                }
-            }
-        }
-    }
-    m_overlap_rhs.insert(pair, false);
-    return false;
+    return result;
 }
 
+
 // Equation is of the form x ++ xs = y1 ++ ys ++ y2 where xs, ys are units.
 // If xs and ys cannot align then
 //     x ++ xs = y1 ++ ys ++ y2 => x = y1 ++ ys ++ z, z ++ xs = y2
@@ -1365,7 +1302,7 @@ struct remove_obj_pair_map : public trail {
    x = pre(x, idx) ++ unit(rhs) ++ post(x, idx + 1)
    NB: need 0 <= idx < len(rhs)   
 */
-bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
+bool theory_seq::solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
     expr* s = nullptr, *idx = nullptr;
     if (ls.size() == 1 && m_util.str.is_nth_i(ls[0], s, idx)) {
         rational r;
@@ -1389,32 +1326,4 @@ bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const&
     return false;
 }
 
-/**
-   match 
-   x = unit(nth_i(x,0)) + unit(nth_i(x,1)) + .. + unit(nth_i(x,k-1))
- */
-
-bool theory_seq::solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
-    if (solve_nth_eq2(ls, rs, dep)) {
-        return true;
-    }
-    if (ls.size() != 1 || rs.size() <= 1) {
-        return false;
-    }
-    expr* l = ls.get(0);
-    rational val;
-    if (!get_length(l, val) || val != rational(rs.size())) {
-        return false;
-    }
-    for (unsigned i = 0; i < rs.size(); ++i) {
-        unsigned k = 0;
-        expr* ru = nullptr, *r = nullptr;
-        if (m_util.str.is_unit(rs.get(i), ru) && m_util.str.is_nth_i(ru, r, k) && k == i && r == l) {
-            continue;
-        }
-        return false;
-    }
-    add_solution(l, mk_concat(rs, l->get_sort()), dep);
-    return true;
-}
 
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 5af14cbd6..ef9ed9120 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -116,7 +116,7 @@ namespace smt {
                             SASSERT(proc);
                         }
                         else {
-                            TRACE("model", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
+                            TRACE("model", tout << "creating fresh value for #" << mk_pp(r->get_expr(), m) << "\n";);
                             proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_sort()));
                         }
                     }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 5d4b0eba0..76f939936 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -931,57 +931,6 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
     return true;
 }
 
-bool theory_seq::solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
-    expr* e = nullptr;
-    
-    if (rs.size() == 1 && m_util.str.is_itos(rs[0], e) && solve_itos(e, ls, dep))
-        return true;
-    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 = m_ax.mk_le(n, -1);
-        propagate_lit(dep, 0, nullptr, lit);
-        return true;
-    }
-    expr* u = nullptr;
-    for (expr* r : rs) {
-        if (m_util.str.is_unit(r, u) && !m_is_digit.contains(u)) {
-            m_is_digit.insert(u);
-            m_trail_stack.push(insert_obj_trail<expr>(m_is_digit, u));
-            literal is_digit = m_ax.is_digit(u);
-            if (ctx.get_assignment(is_digit) != l_true) {
-                propagate_lit(dep, 0, nullptr, is_digit);
-            }
-        }
-    }
-
-    expr_ref num(m), digit(m);
-    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, m_ax.mk_ge(digit, 1));
-    }
-    return true;
-}
-
-
 
 bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) {
     expr_ref len1(m), len2(m);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index ec0a55586..a962e08cd 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -464,11 +464,8 @@ namespace smt {
         bool solve_eq(unsigned idx);
         bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
         bool lift_ite(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
-        bool solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         obj_pair_hashtable<expr, expr> m_nth_eq2_cache;
-        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 solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
 
         bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool propagate_max_length(expr* l, expr* r, dependency* dep);
diff --git a/src/util/top_sort.h b/src/util/top_sort.h
index dd4b73600..8f9df7d52 100644
--- a/src/util/top_sort.h
+++ b/src/util/top_sort.h
@@ -97,7 +97,7 @@ public:
 
     void add(T* t, T* s) {
         T_set* tb = nullptr;
-        if (!m_deps.find(t, tb)) {
+        if (!m_deps.find(t, tb) || !tb) {
             tb = alloc(T_set);
             insert(t, tb);
         }