diff --git a/src/smt/params/theory_seq_params.h b/src/smt/params/theory_seq_params.h
index 278efea7e..c08dda98b 100644
--- a/src/smt/params/theory_seq_params.h
+++ b/src/smt/params/theory_seq_params.h
@@ -30,7 +30,7 @@ struct theory_seq_params {
 
 
     theory_seq_params(params_ref const & p = params_ref()):
-        m_split_w_len(true),
+        m_split_w_len(false),
         m_seq_validate(false),
         m_seq_use_derivatives(false),
         m_seq_use_unicode(false)
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 0db03e952..a6e3aaef3 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -458,11 +458,22 @@ bool theory_seq::len_based_split(eq const& e) {
    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;
+    if (branch_ternary_variable()) {
+        TRACE("seq", tout << "branch_ternary_variable\n";);
+        return true;
+    }
+    if (branch_quat_variable()) {
+        TRACE("seq", tout << "branch_quat_variable\n";);
+        return true;
+    }
+    if (branch_variable_mb()) {
+        TRACE("seq", tout << "branch_variable_mb\n";);
+        return true;
+    }
+    if (branch_variable_eq()) {
+        TRACE("seq", tout << "branch_variable_eq\n";);
+        return true;
+    }
     return false;
 }
 
@@ -737,146 +748,109 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
     }
 }
 
-bool theory_seq::branch_ternary_variable1() {
-    int start = ctx.get_random_value();
-    for (unsigned i = 0; i < m_eqs.size(); ++i) {
-        if (branch_ternary_variable(m_eqs[(i + start) % m_eqs.size()]))
-            return true;
-        if (branch_ternary_variable2(m_eqs[(i + start) % m_eqs.size()])) 
-            return true;
-    }
-    return false;
-}
-
-bool theory_seq::branch_ternary_variable2() {
-    int start = ctx.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)) {
+bool theory_seq::branch_ternary_variable() {
+    for (auto const& e : m_eqs) {
+        if (branch_ternary_variable_rhs(e) || branch_ternary_variable_lhs(e)) {
             return true;
         }
     }
     return false;
 }
 
+
 bool theory_seq::eq_unit(expr* l, expr* 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) {
+// exists x, y, rs' != empty s.t.  (ls = x ++ rs ++ y) || (ls = rs' ++ y && rs = x ++ rs')
+bool theory_seq::can_align_from_lhs(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)) {
+    bool result;
+    if (m_overlap_lhs.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]);        
+            bool same = 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 = eq_unit(ls[j], rs[diff + j]);
+                }
+                if (same) {
+                    m_overlap_lhs.insert(pair, true);
+                    return true;
+                }
             }
-            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]);
+            // ls = x ++ rs ++ y, diff = |x|
+            else {
+                unsigned diff = (i + 1) - rs.size();
+                for (unsigned j = 0; same && j < rs.size()-1; ++j) {
+                    same = eq_unit(ls[diff + j], rs[j]);
+                }
+                if (same) {
+                    m_overlap_lhs.insert(pair, true);
+                    return true;
+                }
             }
-            if (same)
-                result.push_back(i);
         }
-#endif
     }
-    m_overlap.insert(pair, result);
-    return result;
+    m_overlap_lhs.insert(pair, false);
+    return false;
 }
 
-// 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) {
+// exists x, y, rs' != empty s.t.  (ls = x ++ rs ++ y) || (ls = x ++ rs' && rs = rs' ++ y)
+bool theory_seq::can_align_from_rhs(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;
+    bool result;
+    if (m_overlap_rhs.find(pair, result)) {
+        return result;
     }
-    unsigned_vector result;
     for (unsigned i = 0; i < ls.size(); ++i) {
-        if (eq_unit(ls[i], rs[0])) {
+        unsigned diff = ls.size()-1-i;
+        if (eq_unit(ls[diff], 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;
+            // ls = x ++ rs' && rs = rs' ++ y, diff = |x|
+            if (rs.size() > i) {
+                for (unsigned j = 1; same && j <= i; ++j) {
+                    same = eq_unit(ls[diff+j], rs[j]);
+                }
+                if (same) {
+                    m_overlap_rhs.insert(pair, true);
+                    return true;
                 }
-                ++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 const& indexes,
-    expr* x, expr_ref_vector const& xs, expr* y1, expr_ref_vector const& ys, expr* y2) {
-    bool change = false;
-    for (auto ind : indexes) {
-        TRACE("seq", tout << "ind = " << ind << "\n";);
-        expr_ref xs2E(m);
-        xs2E = mk_concat(xs.size()-ind, xs.c_ptr()+ind, m.get_sort(x));
-        
-        literal lit1 = mk_literal(m_autil.mk_le(mk_len(y2), m_autil.mk_int(xs.size()-ind)));
-        switch (ctx.get_assignment(lit1)) {
-        case l_undef:
-            TRACE("seq", tout << "base case init\n";);
-            ctx.mark_as_relevant(lit1);
-            ctx.force_phase(lit1);
-            change = true;
-            break;
-        case l_true: 
-            TRACE("seq", tout << "base case: true branch\n";);
-            propagate_eq(dep, lit1, y2, xs2E, true);
-            if (ind > ys.size()) {
-                expr_ref xs1E  = mk_concat(ind-ys.size(), xs.c_ptr(), m.get_sort(x));
-                expr_ref xxs1E = mk_concat(x, xs1E);
-                propagate_eq(dep, lit1, xxs1E, y1, true);
-            }
-            else if (ind == ys.size()) {
-                propagate_eq(dep, lit1, x, y1, true);
             }
+            // ls = x ++ rs ++ y, diff = |x|
             else {
-                expr_ref ys1E   = mk_concat(ys.size()-ind, ys.c_ptr(), m.get_sort(x));
-                expr_ref y1ys1E = mk_concat(y1, ys1E);
-                propagate_eq(dep, lit1, x, y1ys1E, true);
+                for (unsigned j = 1; same && j < rs.size(); ++j) {
+                    same = eq_unit(ls[diff + j], rs[j]);
+                }
+                if (same) {
+                    m_overlap_rhs.insert(pair, true);
+                    return true;
+                }
             }
-            return true;
-        default:
-            TRACE("seq", tout << "base case: false branch\n";);
-            break;
         }
     }
-    return change;
+    m_overlap_rhs.insert(pair, false);
+    return false;
 }
 
 // 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) {
+// If xs and ys cannot align then
+//     x ++ xs = y1 ++ ys ++ y2 => x = y1 ++ ys ++ z, z ++ xs = y2
+bool theory_seq::branch_ternary_variable_rhs(eq const& e) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x(m), y1(m), y2(m);
-    if (!is_ternary_eq(e.ls(), e.rs(), x, xs, y1, ys, y2, flag1) && 
-        !is_ternary_eq(e.rs(), e.ls(), x, xs, y1, ys, y2, flag1)) {
+    if (!is_ternary_eq_rhs(e.ls(), e.rs(), x, xs, y1, ys, y2) &&
+        !is_ternary_eq_rhs(e.rs(), e.ls(), x, xs, y1, ys, y2)) {
         return false;
     }
 
@@ -892,90 +866,34 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
     }
 
     SASSERT(!xs.empty() && !ys.empty());
-    unsigned_vector indexes = overlap(xs, ys);
-    if (branch_ternary_variable_base(e.dep(), indexes, x, xs, y1, ys, y2))
+    if (!can_align_from_lhs(xs, ys)) {
+        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_r(xsE, y1, ysE, y2);
+        expr_ref ZxsE = mk_concat(Z, xsE);
+        expr_ref y1ysZ = mk_concat(y1ys, Z);
+
+        dependency* dep = e.dep();
+        propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y2), xs.size()));
+        propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y1)), ys.size()));
+        propagate_eq(dep, x, y1ysZ, true);
+        propagate_eq(dep, y2, ZxsE, true);
         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;
     }
-
-    literal ge = m_ax.mk_ge(mk_len(y2), xs.size());
-    dependency* dep = e.dep();
-    switch (ctx.get_assignment(ge)) {
-    case l_undef:
-        TRACE("seq", tout << "rec case init\n";);
-        ctx.mark_as_relevant(ge);
-        ctx.force_phase(ge);
-        break;
-    case l_true:
-        TRACE("seq", tout << "true branch\n";);
-        TRACE("seq", display_equation(tout, e););
-        propagate_eq(dep, ge, x, y1ysZ, true);
-        propagate_eq(dep, ge, y2, ZxsE, true);
-        break;
-    default:
-        return branch_ternary_variable_base(dep, indexes, x, xs, y1, ys, y2);
-    }
-    return true;
-}
-
-bool theory_seq::branch_ternary_variable_base2(
-    dependency* dep, unsigned_vector const& indexes,
-    expr_ref_vector const& xs, expr* x, expr* y1, expr_ref_vector const& ys, expr* y2) {
-    sort* srt = m.get_sort(x);
-    bool change = false;
-    for (auto ind : indexes) {
-        expr_ref xs1E = mk_concat(ind, xs.c_ptr(), m.get_sort(x));
-        literal le = m_ax.mk_le(mk_len(y1), ind);
-        switch (ctx.get_assignment(le)) {
-        case l_undef:
-            TRACE("seq", tout << "base case init\n";);
-            ctx.mark_as_relevant(le);
-            ctx.force_phase(le);
-            change = true;
-            break;
-        case l_true: 
-            TRACE("seq", tout << "base case: true branch\n";);
-            propagate_eq(dep, le, y1, xs1E, true);
-            if (xs.size() - ind > ys.size()) {
-                expr_ref xs2E = mk_concat(xs.size()-ind-ys.size(), xs.c_ptr()+ind+ys.size(), srt);
-                expr_ref xs2x = mk_concat(xs2E, x);
-                propagate_eq(dep, le, xs2x, y2, true);
-            }
-            else if (xs.size() - ind == ys.size()) {
-                propagate_eq(dep, le, x, y2, true);
-            }
-            else {
-                expr_ref ys1E  = mk_concat(ys.size()-xs.size()+ind, ys.c_ptr()+xs.size()-ind, srt);
-                expr_ref ys1y2 = mk_concat(ys1E, y2);
-                propagate_eq(dep, le, x, ys1y2, true);
-            }
-            return true;
-        default:
-            TRACE("seq", tout << "base case: false branch\n";);
-            break;
-        }
-    }
-    return change;
+    return false;
 }
 
 // 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) {
+// If xs and ys cannot align then
+//      xs ++ x = y1 ++ ys ++ y2 => xs ++ z = y1, x = z ++ ys ++ y2
+bool theory_seq::branch_ternary_variable_lhs(eq const& e) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x(m), y1(m), y2(m);
-    if (!is_ternary_eq2(e.ls(), e.rs(), xs, x, y1, ys, y2, flag1) && 
-        !is_ternary_eq2(e.rs(), e.ls(), xs, x, y1, ys, y2, flag1))
+    if (!is_ternary_eq_lhs(e.ls(), e.rs(), xs, x, y1, ys, y2) &&
+        !is_ternary_eq_lhs(e.rs(), e.ls(), xs, x, y1, ys, y2))
         return false;
 
-    dependency* dep = e.dep();
     rational lenX, lenY1, lenY2;
     if (!get_length(x, lenX)) {
         add_length_to_eqc(x);
@@ -987,43 +905,23 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
         add_length_to_eqc(y2);
     }
     SASSERT(!xs.empty() && !ys.empty());
-    unsigned_vector indexes = overlap2(xs, ys);
-    if (branch_ternary_variable_base2(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;
-        propagate_eq(dep, lits, x, Zysy2, true);
-        propagate_eq(dep, lits, y1, xsZ, true);
-    }
-    else {
-        literal ge = m_ax.mk_ge(mk_len(y1), xs.size());
-        switch (ctx.get_assignment(ge)) {
-        case l_undef:
-            TRACE("seq", tout << "rec case init\n";);
-            ctx.mark_as_relevant(ge);
-            ctx.force_phase(ge);
-            break;
-        case l_true:
-            TRACE("seq", display_equation(tout << "true branch\n", e););
-            propagate_eq(dep, ge, x,  Zysy2, true);
-            propagate_eq(dep, ge, y1, xsZ, true);
-            break;
-        default:
-            return branch_ternary_variable_base2(dep, indexes, xs, x, y1, ys, y2);
-        }
-    }
 
-    return true;
+    if (!can_align_from_rhs(xs, ys)) {
+        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_l(xsE, y1, ysE, y2);
+        expr_ref xsZ = mk_concat(xsE, Z);
+        expr_ref Zysy2 = mk_concat(Z, ysy2);
+
+        dependency* dep = e.dep();
+        propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y1), xs.size()));
+        propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y2)), ys.size()));
+        propagate_eq(dep, x, Zysy2, true);
+        propagate_eq(dep, y1, xsZ, true);
+        return true;
+    }
+    return false;
 }
 
 bool theory_seq::branch_quat_variable() {
@@ -1035,14 +933,34 @@ bool theory_seq::branch_quat_variable() {
     return false;
 }
 
+/*
+ * Two properties of align_m
+ *      align_m(align_m(x1, x, _, _), align_m(y1, x, _, _), z, t) = align_m(x1, y1, z, t)
+ *      align_m(x1, x, _, _) - align_m(y1, x, _, _) = x1 - y1
+ */
+literal theory_seq::mk_alignment(expr* e1, expr* e2) {
+    if (m_sk.is_align(e1) && m_sk.is_align(e2)) {
+        expr* x1 = to_app(e1)->get_arg(0);
+        expr* x2 = to_app(e1)->get_arg(1);
+        expr* y1 = to_app(e2)->get_arg(0);
+        expr* y2 = to_app(e2)->get_arg(1);
+        if (x2 == y2 && x1 != y1) {
+            return mk_alignment(x1, y1);
+        }
+    }
+    return mk_simplified_literal(m_autil.mk_le(mk_sub(mk_len(e1), mk_len(e2)), m_autil.mk_int(0)));
+}
+
 // Equation is of the form x1 ++ xs ++ x2 = y1 ++ ys ++ y2 where xs, ys are units.
+// If xs and ys cannot align then
+//      x1 ++ xs ++ x2 = y1 ++ ys ++ y2 =>    |x1| >= |y1 ++ ys|  V  |x1 ++ xs| <= |y1|
 bool theory_seq::branch_quat_variable(eq const& e) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x1(m), x2(m), y1(m), y2(m);
     if (!is_quat_eq(e.ls(), e.rs(), x1, xs, x2, y1, ys, y2))
         return false;
     dependency* dep = e.dep();
-    
+
     rational lenX1, lenX2, lenY1, lenY2;
     if (!get_length(x1, lenX1)) {
         add_length_to_eqc(x1);
@@ -1057,48 +975,119 @@ bool theory_seq::branch_quat_variable(eq const& e) {
         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 sub(mk_sub(mk_len(x1), mk_len(y1)), m);
-    literal le = m_ax.mk_le(sub, 0);
 
-    switch (ctx.get_assignment(le)) {
-    case l_undef:
-        TRACE("seq", tout << "init branch\n";);
-        TRACE("seq", display_equation(tout, e););
-        ctx.mark_as_relevant(le);
-        ctx.force_phase(le);
-        break;
-    case 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);
-        propagate_eq(dep, ~le, x1, y1Z1, true);
-        propagate_eq(dep, ~le, Z1xsx2, ysy2, true);
-        break;
+    bool cond = false;
+
+    // xs and ys cannot align
+    if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys))
+        cond = true;
+    // xs = ys and xs and ys cannot align except the case xs = ys
+    else if (xs == ys) {
+        expr_ref_vector xs1(m), xs2(m);
+        xs1.reset();
+        xs1.append(xs.size()-1, xs.c_ptr()+1);
+        xs2.reset();
+        xs2.append(xs.size()-1, xs.c_ptr());
+        if (!can_align_from_lhs(xs2, ys) && !can_align_from_rhs(xs1, ys))
+            cond = true;
     }
-    case 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);
-        propagate_eq(dep, le, x1Z2, y1, true);
-        propagate_eq(dep, le, xsx2, Z2ysy2, true);
-        break;
+
+    if (cond) {
+        literal_vector lits;
+        if (xs == ys) {
+            literal lit = mk_eq(mk_len(x1), mk_len(y1), false);
+            if (ctx.get_assignment(lit) == l_undef) {
+                TRACE("seq", tout << mk_pp(x1, m) << " = " << mk_pp(y1, m) << "?\n";);
+                ctx.mark_as_relevant(lit);
+                return true;
+            }
+            else if (ctx.get_assignment(lit) == l_true) {
+                TRACE("seq", tout << mk_pp(x1, m) << " = " << mk_pp(y1, m) << "\n";);
+                propagate_eq(dep, lit, x1, y1, true);
+                propagate_eq(dep, lit, x2, y2, true);
+                return true;
+            }
+            TRACE("seq", tout << mk_pp(x1, m) << " != " << mk_pp(y1, m) << "\n";);
+            lits.push_back(~lit);
+        }
+
+        literal lit1 = mk_alignment(x1, y1);
+        literal lit2 = m_ax.mk_ge(mk_sub(mk_len(y1), mk_len(x1)), xs.size());
+        literal lit3 = m_ax.mk_ge(mk_sub(mk_len(x1), mk_len(y1)), ys.size());
+        if (ctx.get_assignment(lit1) == l_undef) {
+            TRACE("seq", tout << mk_pp(x1, m) << " <= " << mk_pp(y1, m) << "?\n";);
+            ctx.mark_as_relevant(lit1);
+            return true;
+        }
+        if (ctx.get_assignment(lit1) == l_true) {
+            TRACE("seq", tout << mk_pp(x1, m) << " <= " << mk_pp(y1, m) << "\n";);
+            if (ctx.get_assignment(lit2) == l_undef) {
+                ctx.mark_as_relevant(lit2);
+                return true;
+            }
+        }
+        else {
+            TRACE("seq", tout << mk_pp(x1, m) << " > " << mk_pp(y1, m) << "\n";);
+            if (ctx.get_assignment(lit3) == l_undef) {
+                ctx.mark_as_relevant(lit3);
+                return true;
+            }
+        }
+
+        expr_ref xsE = mk_concat(xs);
+        expr_ref ysE = mk_concat(ys);
+        expr_ref x1xs = mk_concat(x1, xsE);
+        expr_ref y1ys = mk_concat(y1, ysE);
+        expr_ref xsx2 = mk_concat(xsE, x2);
+        expr_ref ysy2 = mk_concat(ysE, y2);
+        if (ctx.get_assignment(lit1) == l_true && ctx.get_assignment(lit2) == l_true) {
+            // |x1++xs| <= |y1| => x1 ++ xs ++ z2 = y1, x2 = z2 ++ ys ++ y2
+            expr_ref Z2 = m_sk.mk_align_m(y1, x1, xsE, x2);
+            expr_ref x1xsZ2 = mk_concat(x1xs, Z2);
+            expr_ref Z2ysy2 = mk_concat(Z2, ysy2);
+            propagate_eq(dep, lit2, x1xsZ2, y1, true);
+            propagate_eq(dep, lit2, x2, Z2ysy2, true);
+            return true;
+        }
+        if (ctx.get_assignment(lit1) == l_false && ctx.get_assignment(lit3) == l_true) {
+            // |x1| >= |y1++ys| => x1 = y1 ++ ys ++ z1, z1 ++ xs ++ x2 = y2
+            expr_ref Z1 = m_sk.mk_align_m(x1, y1, ysE, y2);
+            expr_ref y1ysZ1 = mk_concat(y1ys, Z1);
+            expr_ref Z1xsx2 = mk_concat(Z1, xsx2);
+            propagate_eq(dep, lit3, x1, y1ysZ1, true);
+            propagate_eq(dep, lit3, Z1xsx2, y2, true);
+            return true;
+        }
+        // Infeasible cases because xs and ys cannot align
+        if (ctx.get_assignment(lit1) == l_false && ctx.get_assignment(lit2) == l_true) {
+            lits.push_back(~lit1);
+            lits.push_back(lit2);
+            propagate_lit(nullptr, lits.size(), lits.c_ptr(), false_literal);
+            return true;
+        }
+        if (ctx.get_assignment(lit1) == l_true && ctx.get_assignment(lit3) == l_true) {
+            lits.push_back(lit1);
+            lits.push_back(lit3);
+            propagate_lit(nullptr, lits.size(), lits.c_ptr(), false_literal);
+            return true;
+        }
+        if (ctx.get_assignment(lit1) == l_true && ctx.get_assignment(lit2) == l_false) {
+            lits.push_back(lit1);
+            lits.push_back(~lit2);
+            propagate_lit(dep, lits.size(), lits.c_ptr(), false_literal);
+            return true;
+        }
+        if (ctx.get_assignment(lit1) == l_false && ctx.get_assignment(lit3) == l_false) {
+            lits.push_back(~lit1);
+            lits.push_back(~lit3);
+            propagate_lit(dep, lits.size(), lits.c_ptr(), false_literal);
+            return true;
+        }
+        UNREACHABLE();
     }
-    }
-    return true;
+    return false;
 }
 
-
 int theory_seq::find_fst_non_empty_idx(expr_ref_vector const& xs) {
     for (unsigned i = 0; i < xs.size(); ++i) {
         expr* x = xs[i];
@@ -1478,8 +1467,8 @@ bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const&
   match: X abc Y..Y' = Z def T..T', where X,Z are variables or concatenation of variables
 */
 
-bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
-                            expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, 
+bool theory_seq::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) {
     if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
         rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
@@ -1494,6 +1483,7 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
             if (!m_util.str.is_unit(ls[l_end])) break;
         }
         --l_end;
+        if (l_end < l_start) return false;
         unsigned r_start = 1;
         for (; r_start < rs.size()-1; ++r_start) {
             if (m_util.str.is_unit(rs[r_start])) break;
@@ -1504,12 +1494,7 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
             if (!m_util.str.is_unit(rs[r_end])) break;
         }
         --r_end;
-        for (unsigned i = l_start; i < l_end+1; ++i) {
-            if (!m_util.str.is_unit(ls[i])) return false;
-        }
-        for (unsigned i = r_start; i < r_end+1; ++i) {
-            if (!m_util.str.is_unit(rs[i])) return false;
-        }
+        if (r_end < r_start) return false;
         xs.reset();
         xs.append(l_end-l_start+1, ls.c_ptr()+l_start);
         x1 = mk_concat(l_start, ls.c_ptr(), srt);
@@ -1524,16 +1509,13 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
 }
 
 /*
-  match: X..X' abc  = Y..Y' mnp Z  // flag1 = false
-         e..X  abc  = Y..Y' mnp Z  // flag1 = true
-   
+  match: .. X abc  = .. Y def Z
          where Z is a variable or concatenation of variables
 */
 
-bool theory_seq::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) {
-    if (ls.size() > 1 && (is_var(ls[0]) || flag1) &&
-        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+bool theory_seq::is_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 (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
         sort* srt = m.get_sort(ls[0]);
         unsigned l_start = ls.size()-1;
         for (; l_start > 0; --l_start) {
@@ -1551,12 +1533,7 @@ bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const&
             if (!m_util.str.is_unit(rs[r_start])) break;
         }
         ++r_start;
-        for (unsigned i = l_start; i < ls.size(); ++i) {
-            if (!m_util.str.is_unit(ls[i])) return false;
-        }
-        for (unsigned i = r_start; i < r_end+1; ++i) {
-            if (!m_util.str.is_unit(rs[i])) return false;
-        }
+
         xs.reset();
         xs.append(ls.size()-l_start, ls.c_ptr()+l_start);
         x = mk_concat(l_start, ls.c_ptr(), srt);
@@ -1570,15 +1547,13 @@ bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const&
 }
 
 /*
-  match: abc X..X'  = Y def Z..Z'        // flag1 is false
-         abc X..e   = Y def Z..Z'        // flag1 is true
+  match: abc X ..  = Y def Z ..
          where Y is a variable or concatenation of variables
 */
 
-bool theory_seq::is_ternary_eq2(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 flag1) {
-    if (ls.size() > 1 && (is_var(ls.back()) || flag1) &&
-        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+bool theory_seq::is_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 (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
         sort* srt = m.get_sort(ls[0]);
         unsigned l_start = 0;
         for (; l_start < ls.size()-1; ++l_start) {
@@ -1595,12 +1570,7 @@ bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const
             if (!m_util.str.is_unit(rs[r_end])) break;
         }
         --r_end;
-        for (unsigned i = 0; i < l_start; ++i) {
-            if (!m_util.str.is_unit(ls[i])) return false;
-        }
-        for (unsigned i = r_start; i < r_end+1; ++i) {
-            if (!m_util.str.is_unit(rs[i])) return false;
-        }
+
         xs.reset();
         xs.append(l_start, ls.c_ptr());
         x = mk_concat(ls.size()-l_start, ls.c_ptr()+l_start, srt);
diff --git a/src/smt/seq_skolem.cpp b/src/smt/seq_skolem.cpp
index 5cae70080..843918e51 100644
--- a/src/smt/seq_skolem.cpp
+++ b/src/smt/seq_skolem.cpp
@@ -34,7 +34,6 @@ seq_skolem::seq_skolem(ast_manager& m, th_rewriter& rw):
     m_pre            = "seq.pre";  // (seq.pre s l):  prefix of string s of length l
     m_post           = "seq.post"; // (seq.post s l): suffix of string s of length k, based on extract starting at index i of length l
     m_eq             = "seq.eq";
-    m_seq_align      = "seq.align";
     m_max_unfolding  = "seq.max_unfolding";
     m_length_limit   = "seq.length_limit";
     m_is_empty       = "re.is_empty";
diff --git a/src/smt/seq_skolem.h b/src/smt/seq_skolem.h
index b25c3d563..1d26f2e16 100644
--- a/src/smt/seq_skolem.h
+++ b/src/smt/seq_skolem.h
@@ -39,7 +39,6 @@ namespace smt {
         symbol         m_is_empty, m_is_non_empty;        // regex emptiness check
         symbol         m_pre, m_post;                     // inverse of at: (pre s i) + (at s i) + (post s i) = s if 0 <= i < (len s)
         symbol         m_eq;                              // equality atom
-        symbol         m_seq_align;
         symbol         m_max_unfolding, m_length_limit;
 
     public:
@@ -58,7 +57,20 @@ namespace smt {
             return mk(symbol(s), e1, e2, e3, e4, range);
         }
 
-        expr_ref mk_align(expr* e1, expr* e2, expr* e3, expr* e4) { return mk(m_seq_align, e1, e2, e3, e4); }
+        expr_ref mk_align(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align", e1, e2, e3, e4); }
+        expr_ref mk_align_l(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align.l", e1, e2, e3, e4); }
+        expr_ref mk_align_r(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align.r", e1, e2, e3, e4); }
+        expr_ref mk_align_m(expr* e1, expr* e2, expr* e3, expr* e4) {
+            if (is_align(e1) && is_align(e2)) {
+                expr* x1 = to_app(e1)->get_arg(0);
+                expr* x2 = to_app(e1)->get_arg(1);
+                expr* y1 = to_app(e2)->get_arg(0);
+                expr* y2 = to_app(e2)->get_arg(1);
+                if (x2 == y2 && x1 != y1)
+                    return mk_align_m(x1, y1, e3, e4);
+            }
+            return mk("seq.align.m", e1, e2, e3, e4);
+        }
         expr_ref mk_accept(expr_ref_vector const& args) { return expr_ref(seq.mk_skolem(m_accept, args.size(), args.c_ptr(), m.mk_bool_sort()), m); }
         expr_ref mk_accept(expr* s, expr* i, expr* r) { return mk(m_accept, s, i, r, nullptr, m.mk_bool_sort()); }
         expr_ref mk_is_non_empty(expr* r, expr* u) { return mk(m_is_non_empty, r, u, m.mk_bool_sort()); }
@@ -112,6 +124,7 @@ namespace smt {
                  r = to_app(e)->get_arg(2), true) && 
                 a.is_unsigned(i, idx);
         }
+        bool is_align(expr* e) const { return is_skolem(symbol("seq.align.m"), e); }
         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;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 4ee901d10..71797fe2f 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -281,8 +281,8 @@ theory_seq::theory_seq(context& ctx):
     m_eq_id(0),
     m_find(*this),
     m_offset_eq(*this, m),
-    m_overlap(m),
-    m_overlap2(m),
+    m_overlap_lhs(m),
+    m_overlap_rhs(m),
     m_factory(nullptr),
     m_exclude(m),
     m_axioms(m),
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index f8b5dc0db..84afa4cc0 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -382,8 +382,8 @@ namespace smt {
         th_union_find              m_find;
         seq_offset_eq              m_offset_eq;
 
-        obj_ref_map<ast_manager, expr, unsigned_vector>    m_overlap;
-        obj_ref_map<ast_manager, expr, unsigned_vector>    m_overlap2;
+        obj_ref_map<ast_manager, expr, bool>    m_overlap_lhs;
+        obj_ref_map<ast_manager, expr, bool>    m_overlap_rhs;
 
 
         seq_factory*               m_factory;    // value factory
@@ -476,8 +476,7 @@ namespace smt {
         bool branch_unit_variable();     // branch on XYZ = abcdef
         bool branch_binary_variable();   // branch on abcX = Ydefg 
         bool branch_variable();          // branch on 
-        bool branch_ternary_variable1(); // branch on XabcY = Zdefg 
-        bool branch_ternary_variable2(); // branch on XabcY = defgZ 
+        bool branch_ternary_variable(); // branch on XabcY = Zdefg 
         bool branch_quat_variable();     // branch on XabcY = ZdefgT
         bool len_based_split();          // split based on len offset
         bool branch_variable_mb();       // branch on a variable, model based on length
@@ -492,14 +491,11 @@ namespace smt {
         bool branch_variable_eq(eq const& e);
         bool branch_binary_variable(eq const& e);
         bool eq_unit(expr* l, expr* r) const;       
-        unsigned_vector overlap(expr_ref_vector const& ls, expr_ref_vector const& rs);
-        unsigned_vector overlap2(expr_ref_vector const& ls, expr_ref_vector const& rs);
-        bool branch_ternary_variable_base(dependency* dep, unsigned_vector const & indexes, expr * x, 
-                                          expr_ref_vector const& xs, expr * y1, expr_ref_vector const& ys, expr * y2);
-        bool branch_ternary_variable_base2(dependency* dep, unsigned_vector const& indexes, expr_ref_vector const& xs, 
-                                           expr * x, expr * y1, expr_ref_vector const& ys, expr * y2);
-        bool branch_ternary_variable(eq const& e, bool flag1 = false);
-        bool branch_ternary_variable2(eq const& e, bool flag1 = false);
+        bool can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs);
+        bool can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs);
+        bool branch_ternary_variable_rhs(eq const& e);
+        bool branch_ternary_variable_lhs(eq const& e);
+        literal mk_alignment(expr* e1, expr* e2);
         bool branch_quat_variable(eq const& e);
         bool len_based_split(eq const& e);
         bool is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs);
@@ -526,8 +522,9 @@ namespace smt {
         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);
-        bool is_ternary_eq2(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 flag1);
+        bool is_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 is_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 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);