diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 568836abb..af5ef3b0b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -470,7 +470,7 @@ br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
     if (bvu.is_bv(e) && bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
         // convert to string constant
         zstring str(n_val.get_unsigned());
-        TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
+        TRACE("seq_verbose", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
         result = m_util.str.mk_string(str);
         return BR_DONE;
     }
diff --git a/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt
index c965f0a62..4beec80f0 100644
--- a/src/smt/params/CMakeLists.txt
+++ b/src/smt/params/CMakeLists.txt
@@ -8,6 +8,7 @@ z3_add_component(smt_params
     theory_array_params.cpp
     theory_bv_params.cpp
     theory_pb_params.cpp
+    theory_seq_params.cpp
     theory_str_params.cpp
   COMPONENT_DEPENDENCIES
     ast
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 32b634626..8901697b7 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -26,6 +26,7 @@ Revision History:
 #include "smt/params/theory_array_params.h"
 #include "smt/params/theory_bv_params.h"
 #include "smt/params/theory_str_params.h"
+#include "smt/params/theory_seq_params.h"
 #include "smt/params/theory_pb_params.h"
 #include "smt/params/theory_datatype_params.h"
 #include "smt/params/preprocessor_params.h"
@@ -79,6 +80,7 @@ struct smt_params : public preprocessor_params,
                     public theory_array_params,
                     public theory_bv_params,
                     public theory_str_params,
+                    public theory_seq_params,
                     public theory_pb_params,
                     public theory_datatype_params {
     bool             m_display_proof;
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 816764896..3f4105c34 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -71,6 +71,7 @@ def_module_params(module_name='smt',
                           ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
                           ('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'),
                           ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
+                          ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
                           ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),
                           ('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'),
                           ('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'),
diff --git a/src/smt/params/theory_seq_params.cpp b/src/smt/params/theory_seq_params.cpp
new file mode 100644
index 000000000..e521298d3
--- /dev/null
+++ b/src/smt/params/theory_seq_params.cpp
@@ -0,0 +1,23 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    theory_seq_params.cpp
+
+Abstract:
+
+    Parameters for sequence theory plugin
+
+Revision History:
+
+
+--*/
+
+#include "smt/params/theory_seq_params.h"
+#include "smt/params/smt_params_helper.hpp"
+
+void theory_seq_params::updt_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_split_w_len = p.seq_split_w_len();
+}
diff --git a/src/smt/params/theory_seq_params.h b/src/smt/params/theory_seq_params.h
new file mode 100644
index 000000000..24e67b8ff
--- /dev/null
+++ b/src/smt/params/theory_seq_params.h
@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    theory_seq_params.h
+
+Abstract:
+
+    Parameters for sequence theory plugin
+
+Revision History:
+
+
+--*/
+
+#ifndef THEORY_SEQ_PARAMS_H
+#define THEORY_SEQ_PARAMS_H
+
+#include "util/params.h"
+
+struct theory_seq_params {
+    /*
+     * Enable splitting guided by length constraints
+     */
+    bool m_split_w_len;
+
+
+    theory_seq_params(params_ref const & p = params_ref()):
+        m_split_w_len(true)
+    {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & p);
+};
+
+#endif /* THEORY_SEQ_PARAMS_H */
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index b90f08cd3..6e996e409 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -222,7 +222,7 @@ namespace smt {
     void setup::setup_QF_BVRE() {
         setup_QF_BV();
         setup_QF_LIA();
-        m_context.register_plugin(alloc(theory_seq, m_manager));
+        m_context.register_plugin(alloc(theory_seq, m_manager, m_params));
     }
 
     void setup::setup_QF_UF(static_features const & st) {        
@@ -721,8 +721,18 @@ namespace smt {
     }
 
     void setup::setup_QF_S() {
-        m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
-        m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params));
+        if (m_params.m_string_solver == "z3str3") {
+            setup_str();
+        }
+        else if (m_params.m_string_solver == "seq") {
+            setup_unknown();
+        }
+        else if (m_params.m_string_solver == "auto") {
+            setup_unknown();
+        }
+        else {
+            throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
+        }
     }
 
     bool is_arith(static_features const & st) {
@@ -885,7 +895,7 @@ namespace smt {
     }
 
     void setup::setup_seq() {
-        m_context.register_plugin(alloc(smt::theory_seq, m_manager));
+        m_context.register_plugin(alloc(smt::theory_seq, m_manager, m_params));
     }
 
     void setup::setup_unknown() {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index d5fe54fae..40aae8043 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -191,9 +191,10 @@ void theory_seq::exclusion_table::display(std::ostream& out) const {
 }
 
 
-theory_seq::theory_seq(ast_manager& m):
+theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
     theory(m.mk_family_id("seq")),
     m(m),
+    m_params(params),
     m_rep(m, m_dm),
     m_reset_cache(false),
     m_eq_id(0),
@@ -215,6 +216,9 @@ theory_seq::theory_seq(ast_manager& m):
     m_atoms_qhead(0),
     m_new_solution(false),
     m_new_propagation(false),
+    m_len_prop_lvl(-1),
+    m_overlap(m),
+    m_overlap2(m),
     m_mk_aut(m) {
     m_prefix         = "seq.p.suffix";
     m_suffix         = "seq.s.prefix";
@@ -230,6 +234,7 @@ theory_seq::theory_seq(ast_manager& m):
     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 l
     m_eq             = "seq.eq";
+    m_seq_align      = "seq.align";
 
 }
 
@@ -264,6 +269,16 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>solve_nqs\n";);
         return FC_CONTINUE;
     }
+    if (fixed_length(true)) {
+        ++m_stats.m_fixed_length;
+        TRACE("seq", tout << ">>zero_length\n";);
+        return FC_CONTINUE;
+    }
+    if (m_params.m_split_w_len && len_based_split()) {
+        ++m_stats.m_branch_variable;
+        TRACE("seq", tout << ">>split_based_on_length\n";);
+        return FC_CONTINUE;
+    }
     if (fixed_length()) {
         ++m_stats.m_fixed_length;
         TRACE("seq", tout << ">>fixed_length\n";);
@@ -284,12 +299,17 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>branch_unit_variable\n";);
         return FC_CONTINUE;
     }
-    if (branch_binary_variable() || branch_variable_mb()) {
+    if (branch_binary_variable()) {
         ++m_stats.m_branch_variable;
-        TRACE("seq", tout << ">>branch_variable\n";);
+        TRACE("seq", tout << ">>branch_binary_variable\n";);
         return FC_CONTINUE;
     }
-    if (branch_variable()) {
+    if (branch_ternary_variable1() || branch_ternary_variable2() || branch_quat_variable()) {
+        ++m_stats.m_branch_variable;
+        TRACE("seq", tout << ">>split_based_on_alignment\n";);
+        return FC_CONTINUE;
+    }
+    if (branch_variable_mb() || branch_variable()) {
         ++m_stats.m_branch_variable;
         TRACE("seq", tout << ">>branch_variable\n";);
         return FC_CONTINUE;
@@ -332,7 +352,7 @@ bool theory_seq::reduce_length_eq() {
 }
 
 bool theory_seq::branch_binary_variable() {
-    for (eq const& e : m_eqs) {
+    for (auto const& e : m_eqs) {
         if (branch_binary_variable(e)) {
             TRACE("seq", display_equation(tout, e););
             return true;
@@ -411,7 +431,7 @@ bool theory_seq::branch_binary_variable(eq const& e) {
 
 bool theory_seq::branch_unit_variable() {
     bool result = false;
-    for (eq const& e : m_eqs) {
+    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;
@@ -434,8 +454,8 @@ 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 (expr* r : rs) {
-        if (!m_util.str.is_unit(r)) {
+    for (auto const& elem : rs) {
+        if (!m_util.str.is_unit(elem)) {
             return false;
         }
     }
@@ -478,9 +498,874 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
     }
 }
 
+bool theory_seq::branch_ternary_variable1() {
+    for (auto const& e : m_eqs) {
+        if (branch_ternary_variable(e) || branch_ternary_variable2(e)) {
+            return true;
+        }
+    }
+    return false;
+}
+
+bool theory_seq::branch_ternary_variable2() {
+    for (auto const& e : m_eqs) {
+        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')
+unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector const& rs) {
+    SASSERT(!ls.empty() && !rs.empty());
+    unsigned_vector res;
+    expr* l = mk_concat(ls);
+    expr* r = mk_concat(rs);
+    expr* pair = m.mk_eq(l,r);
+    if (m_overlap.find(pair, res)) {
+        return res;
+    }
+    unsigned_vector result;
+    for (unsigned i = 0; i < ls.size(); ++i) {
+        if (eq_unit(ls[i], rs.back())) {
+            bool same = true;
+            if (i >= 1) {
+                for (unsigned j = i-1; j>=0 && rs.size()+j-i>=1; --j) {
+                    if (!eq_unit(ls[j], rs[rs.size()+j-i-1])) {
+                        same = false;
+                        break;
+                    }
+                }
+                if (same)
+                    result.push_back(i+1);
+            }
+            else 
+                result.push_back(1);
+        }
+    }
+    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* l = mk_concat(ls);
+    expr* r = mk_concat(rs);
+    expr* pair = m.mk_eq(l,r);
+    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(m_util.str.mk_length(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), m);
+                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), m);
+                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* x = nullptr, *y1 = nullptr, *y2 = nullptr;
+    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)) {
+        enforce_length(ensure_enode(x));
+    }
+    if (!get_length(y1, lenY1)) {
+        enforce_length(ensure_enode(y1));
+    }
+    if (!get_length(y2, lenY2)) {
+        enforce_length(ensure_enode(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), m);
+    expr_ref ysE(mk_concat(ys), m);
+    expr_ref y1ys(mk_concat(y1, ysE));
+    expr_ref Z(mk_skolem(m_seq_align, y2, xsE, x, y1ys), m);
+    expr_ref ZxsE(mk_concat(Z, xsE), m);
+    expr_ref y1ysZ(mk_concat(y1ys, Z), m);
+    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, y1ysZ, true);
+        propagate_eq(dep, lits, y2, ZxsE, true);
+    }
+    else {
+        expr_ref ge(m_autil.mk_ge(m_util.str.mk_length(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(m_util.str.mk_length(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), m);
+                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), m);
+                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* x = nullptr, *y1 = nullptr, *y2 = nullptr;
+    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)) {
+        enforce_length(ensure_enode(x));
+    }
+    if (!get_length(y1, lenY1)) {
+        enforce_length(ensure_enode(y1));
+    }
+    if (!get_length(y2, lenY2)) {
+        enforce_length(ensure_enode(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), m);
+    expr_ref ysE(mk_concat(ys), m);
+    expr_ref ysy2(mk_concat(ysE, y2), m);
+    expr_ref Z(mk_skolem(m_seq_align, x, ysy2, y1, xsE), m);
+    expr_ref xsZ(mk_concat(xsE, Z), m);
+    expr_ref Zysy2(mk_concat(Z, ysy2), m);
+    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(m_util.str.mk_length(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* x1_l = nullptr, *x2 = nullptr, *y1_l = nullptr, *y2 = nullptr;
+    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)) {
+        enforce_length(ensure_enode(x1_l));
+    }
+    if (!get_length(y1_l, lenY1)) {
+        enforce_length(ensure_enode(y1_l));
+    }
+    if (!get_length(x2, lenX2)) {
+        enforce_length(ensure_enode(x2));
+    }
+    if (!get_length(y2, lenY2)) {
+        enforce_length(ensure_enode(y2));
+    }
+    SASSERT(!xs.empty() && !ys.empty());
+    
+    xs.push_back(x2);
+    expr_ref xsx2(mk_concat(xs), m);
+    ys.push_back(y2);
+    expr_ref ysy2(mk_concat(ys), m);
+    expr_ref x1(x1_l, m);
+    expr_ref y1(y1_l, m);
+    expr_ref sub(mk_sub(m_util.str.mk_length(x1_l), m_util.str.mk_length(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(mk_skolem(m_seq_align, ysy2, xsx2, x1, y1), m);
+        expr_ref y1Z1(mk_concat(y1, Z1), m);
+        expr_ref Z1xsx2(mk_concat(Z1, xsx2), m);
+        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(mk_skolem(m_seq_align, xsx2, ysy2, y1, x1), m);
+        expr_ref x1Z2(mk_concat(x1, Z2), m);
+        expr_ref Z2ysy2(mk_concat(Z2, ysy2), m);
+        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* const& 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 = ctx.get_enode(l1)->get_root(), *n1 = r1;
+            enode* r2 = ctx.get_enode(l22)->get_root(), *n2 = r2;
+            expr *e1 = nullptr, *e2 = nullptr;
+            do {
+                if (!m_util.str.is_length(n1->get_owner(), e1))
+                    n1 = n1->get_next();
+                else
+                    break;
+            }
+            while (n1 != r1);
+            do {
+                if (!m_util.str.is_length(n2->get_owner(), e2))
+                    n2 = n2->get_next();
+                else
+                    break;
+            }
+            while (n2 != r2);
+            if (m_util.str.is_length(n1->get_owner(), e1)
+            && m_util.str.is_length(n2->get_owner(), e2)) {
+                obj_map<enode, int> tmp;
+                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) const {
+    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(m_util.str.mk_length(x), m);
+        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) const {
+    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 {
+                lower_bound(ls.get(j), lo);
+                upper_bound(ls.get(j), 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, m_util.str.mk_length(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 {
+                lower_bound(rs.get(j), lo);
+                upper_bound(rs.get(j), 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, m_util.str.mk_length(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 const& 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(m_util.str.mk_length(r_fst), m);
+    enode * root2;
+    if (!ctx.e_internalized(len_r_fst))
+        return false;
+    else
+        root2 = ctx.get_enode(len_r_fst)->get_root();
+
+    // Offset = 0, No change
+    if (l_fst) {
+        expr_ref len_l_fst(m_util.str.mk_length(l_fst), m);
+        if (ctx.e_internalized(len_l_fst)) {
+            enode * root1 = ctx.get_enode(len_l_fst)->get_root();
+            if (root1 == 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().size() == ls.size()) {
+                bool flag = true;
+                for (unsigned j = 0; j < ls.size(); ++j)
+                    if (e.ls().get(j) != ls.get(j)) {
+                        flag = false;
+                        break;
+                    }
+                if (flag) {
+                    expr* nl_fst = 0;
+                    if (e.rs().size()>1 && is_var(e.rs().get(0)))
+                        nl_fst = e.rs().get(0);
+                    if (nl_fst && nl_fst != r_fst) {
+                        expr_ref len_nl_fst(m_util.str.mk_length(nl_fst), m);
+                        if (ctx.e_internalized(len_nl_fst)) {
+                            enode * root1 = ctx.get_enode(len_nl_fst)->get_root();
+                            if (root1 == root2) {
+                                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) {
+        expr_ref len_l_fst(m_util.str.mk_length(l_fst), m);
+        if (ctx.e_internalized(len_l_fst)) {
+            enode * root1 = ctx.get_enode(len_l_fst)->get_root();
+            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().size() == ls.size()) {
+                bool flag = true;
+                for (unsigned j = 0; j < ls.size(); ++j)
+                    if (e.ls().get(j) != ls.get(j)) {
+                        flag = false;
+                        break;
+                    }
+                if (flag) {
+                    expr* nl_fst = 0;
+                    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(m_util.str.mk_length(nl_fst), m);
+                        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.size() == 0 || rs.size() == 0)
+        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_r_fst(m_util.str.mk_length(r_fst), m);
+    enode * root2;
+    if (!ctx.e_internalized(len_r_fst))
+        return false;
+    else
+        root2 = ctx.get_enode(len_r_fst)->get_root();
+
+    expr_ref len_l_fst(m_util.str.mk_length(l_fst), m);
+    if (ctx.e_internalized(len_l_fst)) {
+        enode * root1 = ctx.get_enode(len_l_fst)->get_root();
+        if (root1 == root2) {
+            TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
+            offset = 0;
+            return true;
+        }
+        obj_map<enode, int> tmp;
+        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";);
+                return true;
+            }
+            else 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(m_util.str.mk_length(x11),m);
+    expr_ref lenY11(m);
+    expr_ref Z(m);
+    int offset = 0;
+    if (offset_orig != 0) {
+        lenY11 = m_autil.mk_add(m_util.str.mk_length(y11), m_autil.mk_int(offset_orig));
+        if (offset_orig > 0) {
+            offset = offset_orig;
+            Z = mk_skolem(m_seq_align, y12, x12, x11, y11);
+            y11 = mk_concat(y11, Z);
+            x12 = mk_concat(Z, x12);
+        }
+        else {
+            offset = -offset_orig;
+            Z = mk_skolem(m_seq_align, x12, y12, y11, x11);
+            x11 = mk_concat(x11, Z);
+            y12 = mk_concat(Z, y12);
+        }
+    }
+    else
+        lenY11 = m_util.str.mk_length(y11);
+
+    dependency* dep = e.dep();
+    literal_vector lits;
+    literal lit1 = mk_eq(lenX11, lenY11, 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, m_util.str.mk_length(ls[i]));
+        for (unsigned i = 2; i < rs.size(); ++i)
+            len2 = mk_add(len2, m_util.str.mk_length(rs[i]));
+        bool flag = false;
+        if (!m_autil.is_numeral(len1) && !m_autil.is_numeral(len2)) {
+            literal lit2 = mk_eq(len1, len2, false);
+            flag = ctx.get_assignment(lit2) == l_true;
+        }
+        else {
+            expr_ref eq_len(m.mk_eq(len1, len2), m);
+            flag = ctx.find_assignment(eq_len) == l_true;
+        }
+        
+        if (flag) {
+            literal lit2 = mk_eq(len1, len2, false);
+            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(m_util.str.mk_length(Z), m);
+        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;
+}
+
 bool theory_seq::branch_variable_mb() {
     bool change = false;
-    for (eq const& e : m_eqs) {
+    for (auto const& e : m_eqs) {
         vector<rational> len1, len2;
         if (!is_complex(e)) {
             continue;
@@ -495,12 +1380,12 @@ bool theory_seq::branch_variable_mb() {
             continue;
         }
         rational l1, l2;
-        for (unsigned j = 0; j < len1.size(); ++j) l1 += len1[j];
-        for (unsigned j = 0; j < len2.size(); ++j) l2 += len2[j];
+        for (auto elem : len1) l1 += elem;
+        for (auto elem : len2) l2 += elem;
         if (l1 != l2) {
             TRACE("seq", tout << "lengths are not compatible\n";);
-            expr_ref l = mk_concat(e.ls());
-            expr_ref r = mk_concat(e.rs());
+            expr_ref l(mk_concat(e.ls()), m);
+            expr_ref r(mk_concat(e.rs()), m);
             expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m);
             propagate_eq(e.dep(), lnl, lnr, false);
             change = true;
@@ -519,11 +1404,11 @@ bool theory_seq::branch_variable_mb() {
 
 bool theory_seq::is_complex(eq const& e) {
     unsigned num_vars1 = 0, num_vars2 = 0;
-    for (unsigned i = 0; i < e.ls().size(); ++i) {
-        if (is_var(e.ls()[i])) ++num_vars1;
+    for (auto const& elem : e.ls()) {
+        if (is_var(elem)) ++num_vars1;
     }
-    for (unsigned i = 0; i < e.rs().size(); ++i) {
-        if (is_var(e.rs()[i])) ++num_vars2;
+    for (auto const& elem : e.rs()) {
+        if (is_var(elem)) ++num_vars2;
     }
     return num_vars1 > 0 && num_vars2 > 0 && num_vars1 + num_vars2 > 2;
 }
@@ -875,11 +1760,11 @@ bool theory_seq::propagate_length_coherence(expr* e) {
     if (!is_var(e) || !m_rep.is_root(e)) {
         return false;
     }
-    if (!lower_bound(e, lo) || !lo.is_pos() || lo >= rational(2048)) {
+    if (!lower_bound2(e, lo) || !lo.is_pos() || lo >= rational(2048)) {
         return false;
     }
     TRACE("seq", tout << "Unsolved " << mk_pp(e, m);
-          if (!lower_bound(e, lo)) lo = -rational::one();
+          if (!lower_bound2(e, lo)) lo = -rational::one();
           if (!upper_bound(e, hi)) hi = -rational::one();
           tout << " lo: " << lo << " hi: " << hi << "\n";
           );
@@ -950,13 +1835,13 @@ bool theory_seq::check_length_coherence0(expr* e) {
 bool theory_seq::check_length_coherence() {
 
 #if 1
-    for (expr* e : m_length) {
+    for (auto e : m_length) {
         if (check_length_coherence0(e)) {
             return true;
         }
     }
 #endif
-    for (expr* e : m_length) {
+    for (auto e : m_length) {
         if (check_length_coherence(e)) {
             return true;
         }
@@ -964,19 +1849,20 @@ bool theory_seq::check_length_coherence() {
     return false;
 }
 
-bool theory_seq::fixed_length() {
+bool theory_seq::fixed_length(bool is_zero) {
     bool found = false;
-    for (expr* e : m_length) {
-        if (fixed_length(e)) {
+    for (auto e : m_length) {
+        if (fixed_length(e, is_zero)) {
             found = true;
         }
     }
     return found;
 }
 
-bool theory_seq::fixed_length(expr* e) {
+bool theory_seq::fixed_length(expr* e, bool is_zero) {
     rational lo, hi;
-    if (!(is_var(e) && lower_bound(e, lo) && upper_bound(e, hi) && lo == hi && lo.is_unsigned())) {
+    if (!(is_var(e) && lower_bound(e, lo) && upper_bound(e, hi) && lo == hi
+    && ((is_zero && lo.is_zero()) || (!is_zero && lo.is_unsigned())))) {
         return false;
     }
     if (is_skolem(m_tail, e) || is_skolem(m_seq_first, e) || 
@@ -996,7 +1882,7 @@ bool theory_seq::fixed_length(expr* e) {
     if (lo.is_zero()) {
         seq = m_util.str.mk_empty(m.get_sort(e));
     }
-    else {
+    else if (!is_zero) {
         unsigned _lo = lo.get_unsigned();
         expr_ref_vector elems(m);
         
@@ -1039,6 +1925,11 @@ bool theory_seq::propagate_is_conc(expr* e, expr* conc) {
     }
 }
 
+bool theory_seq::is_unit_nth(expr* e) const {
+    expr *s = nullptr;
+    return m_util.str.is_unit(e, s) && is_nth(s);
+}
+
 bool theory_seq::is_nth(expr* e) const {
     return is_skolem(m_nth, e);
 }
@@ -1080,11 +1971,11 @@ bool theory_seq::is_post(expr* e, expr*& s, expr*& i) {
 expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
     sort* char_sort = nullptr;
     VERIFY(m_util.is_seq(m.get_sort(s), char_sort));
-    return mk_skolem(m_nth, s, idx, nullptr, char_sort);
+    return mk_skolem(m_nth, s, idx, nullptr, nullptr, char_sort);
 }
 
 expr_ref theory_seq::mk_sk_ite(expr* c, expr* t, expr* e) {
-    return mk_skolem(symbol("seq.if"), c, t, e, m.get_sort(t));
+    return mk_skolem(symbol("seq.if"), c, t, e, nullptr, m.get_sort(t));
 }
 
 expr_ref theory_seq::mk_last(expr* s) {
@@ -1094,7 +1985,7 @@ expr_ref theory_seq::mk_last(expr* s) {
     }
     sort* char_sort = nullptr;
     VERIFY(m_util.is_seq(m.get_sort(s), char_sort));
-    return mk_skolem(m_seq_last, s, nullptr, nullptr, char_sort);
+    return mk_skolem(m_seq_last, s, nullptr, nullptr, nullptr, char_sort);
 }
 
 expr_ref theory_seq::mk_first(expr* s) {
@@ -1412,6 +2303,10 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const&
     if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, m.get_sort(r[0])), deps)) {
         return true;
     }
+//    if (l.size() == 1 && r.size() == 1 && l[0] != r[0] && is_nth(l[0]) && add_solution(l[0], r[0], deps))
+//        return true;
+//    if (l.size() == 1 && r.size() == 1 && l[0] != r[0] && is_nth(r[0]) && add_solution(r[0], l[0], deps))
+//        return true;
 
     return false;
 }
@@ -1440,14 +2335,18 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
     if (is_var(r) && !occurs(r, l) && add_solution(r, l, deps)) {
         return true;
     }
+//    if (is_nth(l) && !occurs(l, r) && add_solution(l, r, deps))
+//        return true;
+//    if (is_nth(r) && !occurs(r, l) && add_solution(r, l, deps))
+//        return true;
 
     return false;
 }
 
 
 bool theory_seq::occurs(expr* a, expr_ref_vector const& b) {
-    for (unsigned i = 0; i < b.size(); ++i) {
-        if (a == b[i] || m.is_ite(b[i])) return true;
+    for (auto const& elem : b) {
+        if (a == elem || m.is_ite(elem)) return true;
     }
     return false;
 }
@@ -1474,7 +2373,7 @@ bool theory_seq::occurs(expr* a, expr* b) {
 }
 
 
-bool theory_seq::is_var(expr* a) {
+bool theory_seq::is_var(expr* a) const {
     return
         m_util.is_seq(a) &&
         !m_util.str.is_concat(a) &&
@@ -1507,7 +2406,7 @@ bool theory_seq::solve_eqs(unsigned i) {
     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())) {
+        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);
@@ -1521,7 +2420,7 @@ bool theory_seq::solve_eqs(unsigned i) {
     return change || m_new_propagation || ctx.inconsistent();
 }
 
-bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
+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;
@@ -1550,8 +2449,26 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
         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";);
-        m_eqs.push_back(eq(m_eq_id++, ls, rs, deps));
+        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));
+        }
         return true;
     }
     return false;
@@ -1591,6 +2508,124 @@ bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const&
     return false;
 }
 
+bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+expr*& x1, expr_ref_vector& xs, expr*& x2, expr*& y1, expr_ref_vector& ys, expr*& 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 l_start = 1;
+        for (; l_start < ls.size()-1; ++l_start) {
+            if (m_util.str.is_unit(ls[l_start])) break;
+        }
+        if (l_start == ls.size()-1) return false;
+        unsigned l_end = l_start;
+        for (; l_end < ls.size()-1; ++l_end) {
+            if (!m_util.str.is_unit(ls[l_end])) break;
+        }
+        --l_end;
+        unsigned r_start = 1;
+        for (; r_start < rs.size()-1; ++r_start) {
+            if (m_util.str.is_unit(rs[r_start])) break;
+        }
+        if (r_start == rs.size()-1) return false;
+        unsigned r_end = r_start;
+        for (; r_end < rs.size()-1; ++r_end) {
+            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;
+        }
+        xs.reset();
+        xs.append(l_end-l_start+1, ls.c_ptr()+l_start);
+        x1 = m_util.str.mk_concat(l_start, ls.c_ptr());
+        x2 = m_util.str.mk_concat(ls.size()-l_end-1, ls.c_ptr()+l_end+1);
+        ys.reset();
+        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
+        y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
+        y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
+        return true;
+    }
+    return false;
+}
+
+bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+expr*& x, expr_ref_vector& xs, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1) {
+    if (ls.size() > 1 && (is_var(ls[0]) || flag1) &&
+        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+        unsigned l_start = ls.size()-1;
+        for (; l_start > 0; --l_start) {
+            if (!m_util.str.is_unit(ls[l_start])) break;
+        }
+        if (l_start == ls.size()-1) return false;
+        ++l_start;
+        unsigned r_end = rs.size()-2;
+        for (; r_end > 0; --r_end) {
+            if (m_util.str.is_unit(rs[r_end])) break;
+        }
+        if (r_end == 0) return false;
+        unsigned r_start = r_end;
+        for (; r_start > 0; --r_start) {
+            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 = m_util.str.mk_concat(l_start, ls.c_ptr());
+        ys.reset();
+        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
+        y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
+        y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
+        return true;
+    }
+    return false;
+}
+
+bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+        expr_ref_vector& xs, expr*& x, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1) {
+    if (ls.size() > 1 && (is_var(ls.back()) || flag1) &&
+        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+        unsigned l_start = 0;
+        for (; l_start < ls.size()-1; ++l_start) {
+            if (!m_util.str.is_unit(ls[l_start])) break;
+        }
+        if (l_start == 0) return false;
+        unsigned r_start = 1;
+        for (; r_start < rs.size()-1; ++r_start) {
+            if (m_util.str.is_unit(rs[r_start])) break;
+        }
+        if (r_start == rs.size()-1) return false;
+        unsigned r_end = r_start;
+        for (; r_end < rs.size()-1; ++r_end) {
+            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 = m_util.str.mk_concat(ls.size()-l_start, ls.c_ptr()+l_start);
+        ys.reset();
+        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
+        y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
+        y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
+        return true;
+    }
+    return false;
+}
+
 bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
     if (ls.empty() || rs.empty()) {
         return false;
@@ -1695,6 +2730,10 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
     expr_ref lenr(m_util.str.mk_length(r), m);
     literal lit = mk_eq(lenl, lenr, false);
     if (ctx.get_assignment(lit) == l_true) {
+//    expr_ref len_eq(m.mk_eq(lenl, lenr), m);
+//    if (ctx.find_assignment(len_eq) == l_true) {
+//        literal lit = mk_eq(lenl, lenr, false);
+//        literal_vector lits;
         expr_ref_vector lhs(m), rhs(m);
         lhs.append(l2, ls2);
         rhs.append(r2, rs2);
@@ -2255,7 +3294,7 @@ bool theory_seq::internalize_term(app* term) {
         return true;
     }
     TRACE("seq_verbose", tout << mk_pp(term, m) << "\n";);
-    for (expr* arg : *term) {
+    for (auto arg : *term) {
         mk_var(ensure_enode(arg));
     }
     if (m.is_bool(term)) {
@@ -2283,7 +3322,7 @@ void theory_seq::add_length(expr* e) {
 
 
 /*
-  ensure that all elements in equivalence class occur under an applicatin of 'length'
+  ensure that all elements in equivalence class occur under an application of 'length'
 */
 void theory_seq::enforce_length(enode* n) {
     enode* n1 = n;
@@ -2405,7 +3444,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
 
 literal theory_seq::is_digit(expr* ch) {
     bv_util bv(m);
-    literal isd = mk_literal(mk_skolem(symbol("seq.is_digit"), ch, nullptr, nullptr, m.mk_bool_sort()));
+    literal isd = mk_literal(mk_skolem(symbol("seq.is_digit"), ch, nullptr, nullptr, nullptr, m.mk_bool_sort()));
     expr_ref d2i = digit2int(ch);
     expr_ref _lo(bv.mk_ule(bv.mk_numeral(rational('0'), bv.mk_sort(8)), ch), m);
     expr_ref _hi(bv.mk_ule(ch, bv.mk_numeral(rational('9'), bv.mk_sort(8))), m);
@@ -2421,7 +3460,7 @@ literal theory_seq::is_digit(expr* ch) {
 }
 
 expr_ref theory_seq::digit2int(expr* ch) {
-    return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, nullptr, nullptr, m_autil.mk_int()), m);
+    return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, nullptr, nullptr, nullptr, m_autil.mk_int()), m);
 }
 
 void theory_seq::add_itos_axiom(expr* e) {
@@ -2519,7 +3558,7 @@ void theory_seq::display(std::ostream & out) const {
     }
 
     if (!m_length.empty()) {
-        for (expr* e : m_length) {
+        for (auto e : m_length) {
             rational lo(-1), hi(-1);
             lower_bound(e, lo);
             upper_bound(e, hi);
@@ -2544,7 +3583,7 @@ void theory_seq::display_nc(std::ostream& out, nc const& nc) const {
 }
 
 void theory_seq::display_equations(std::ostream& out) const {
-    for (eq const& e : m_eqs) {
+    for (auto const& e : m_eqs) {
         display_equation(out, e);
     }
 }
@@ -2640,7 +3679,7 @@ void theory_seq::init_search_eh() {
 
 void theory_seq::init_model(expr_ref_vector const& es) {
     expr_ref new_s(m);
-    for (expr* e : es) {
+    for (auto e : es) {
         dependency* eqs = nullptr;
         expr_ref s = canonize(e, eqs);
         if (is_var(s)) {
@@ -3480,6 +4519,12 @@ expr_ref theory_seq::mk_sub(expr* a, expr* b) {
     return result;
 }
 
+expr_ref theory_seq::mk_add(expr* a, expr* b) {
+    expr_ref result(m_autil.mk_add(a, b), m);
+    m_rewrite(result);
+    return result;
+}
+
 enode* theory_seq::ensure_enode(expr* e) {
     context& ctx = get_context();
     if (!ctx.e_internalized(e)) {
@@ -3540,6 +4585,45 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) const {
     return m_autil.is_numeral(_lo, lo) && lo.is_int();
 }
 
+// The difference with lower_bound function is that since in some cases,
+// the lower bound is not updated for all the enodes in the same eqc,
+// we have to traverse the eqc to query for the better lower bound.
+bool theory_seq::lower_bound2(expr* _e, rational& lo) {
+    context& ctx = get_context();
+    expr_ref e(m_util.str.mk_length(_e), m);
+    expr_ref _lo(m);
+    theory_mi_arith* tha = get_th_arith<theory_mi_arith>(ctx, m_autil.get_family_id(), e);
+    if (!tha) {
+        theory_i_arith* thi = get_th_arith<theory_i_arith>(ctx, m_autil.get_family_id(), e);
+        if (!thi || !thi->get_lower(ctx.get_enode(e), _lo)) return false;
+    }
+    enode *ee = ctx.get_enode(e);
+    if (!tha->get_lower(ee, _lo) || m_autil.is_numeral(_lo, lo)) {
+        enode *next = ee->get_next();
+        bool flag = false;
+        while (next != ee) {
+            if (!m_autil.is_numeral(next->get_owner()) && !m_util.str.is_length(next->get_owner())) {
+                expr *var = next->get_owner();
+                TRACE("seq", tout << mk_pp(var, m) << "\n";);
+                expr_ref _lo2(m);
+                rational lo2;
+                if (tha->get_lower(next, _lo2) && m_autil.is_numeral(_lo2, lo2) && lo2>lo) {
+                    flag = true;
+                    lo = lo2;
+                    literal low(mk_literal(m_autil.mk_ge(var, _lo2)));
+                    add_axiom(~low, mk_literal(m_autil.mk_ge(e, _lo2)));
+                }
+            }
+            next = next->get_next();
+        }
+        if (flag)
+            return true;
+        if (!tha->get_lower(ee, _lo))
+            return false;
+    }
+    return true;
+}
+
 bool theory_seq::upper_bound(expr* _e, rational& hi) const {
     context& ctx = get_context();
     expr_ref e(m_util.str.mk_length(_e), m);
@@ -3847,7 +4931,7 @@ literal theory_seq::mk_literal(expr* _e) {
 
 literal theory_seq::mk_seq_eq(expr* a, expr* b) {
     SASSERT(m_util.is_seq(a));
-    return mk_literal(mk_skolem(m_eq, a, b, nullptr, m.mk_bool_sort()));
+    return mk_literal(mk_skolem(m_eq, a, b, nullptr, nullptr, m.mk_bool_sort()));
 }
 
 literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
@@ -3861,7 +4945,7 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
     }
     expr_ref_vector concats(m);
     m_util.str.get_concat(e, concats);
-    for (expr* c : concats) {
+    for (auto c : concats) {
         if (m_util.str.is_unit(c)) {
             return false_literal;
         }
@@ -3892,13 +4976,73 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
 }
 
+expr* theory_seq::coalesce_chars(expr* const& e) {
+    context& ctx = get_context();
+    expr* s;
+    if (m_util.str.is_concat(e)) {
+        expr_ref_vector concats(m);
+        m_util.str.get_concat(e, concats);
+        expr_ref_vector result(m);
+        for (unsigned i = 0; i < concats.size(); ++i) {
+            expr_ref tmp(coalesce_chars(concats[i].get()), m);
+            if (m_util.str.is_empty(tmp)) continue;
+            zstring zs, a;
+            bool flag = false;
+            while (m_util.str.is_string(tmp, a)) {
+                if (flag)
+                    zs = zs + a;
+                else
+                    zs = a;
+                flag = true;
+                if (i < concats.size()-1)
+                    tmp = coalesce_chars(concats[++i].get());
+                else {
+                    ++i;
+                    break;
+                }
+            }
+            if (flag) {
+                result.push_back(m_util.str.mk_string(zs));
+                if (i < concats.size())
+                    result.push_back(tmp);
+            }
+            else
+                result.push_back(tmp);
+        }
+        SASSERT(result.size() > 0);
+        if (result.size() > 1)
+            return m_util.str.mk_concat(result.size(), result.c_ptr());
+        else 
+            return e;
+    }
+    else if (m_util.str.is_unit(e, s)) {
+        bv_util bvu(m);
+        if (bvu.is_bv(s)) {
+            expr_ref result(m);
+            expr * args[1] = {s};
+            if (m_seq_rewrite.mk_app_core(to_app(e)->get_decl(), 1, args, result)) {
+                if (!ctx.e_internalized(result))
+                    ctx.internalize(result, false);
+                return result;
+            }
+        }
+    }
+    return e;
+}
+
+expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3, expr*e4, sort* range) {
+    expr* es[4] = { e1, e2, e3, e4 };
+    unsigned len = e4?4:(e3?3:(e2?2:1));
 
-expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3, sort* range) {
-    expr* es[3] = { e1, e2, e3 };
-    unsigned len = e3?3:(e2?2:1);
     if (!range) {
         range = m.get_sort(e1);
     }
+    if (name == m_seq_align) {
+        for (unsigned i = 0; i < len; ++i) {
+      	    es[i] = coalesce_chars(es[i]);
+      	    TRACE("seq", tout << mk_pp(es[i], m) << "\n";);
+        }
+    }
     return expr_ref(m_util.mk_skolem(name, len, es, range), m);
 }
 
@@ -4158,6 +5302,10 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
     if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) {
         m_replay.reset();
     }
+    if (m_len_prop_lvl > (int) ctx.get_scope_level()) {
+        m_len_prop_lvl = ctx.get_scope_level();
+        m_len_offset.reset();
+    }
 }
 
 void theory_seq::restart_eh() {
@@ -4509,8 +5657,8 @@ void theory_seq::propagate_not_prefix(expr* e) {
     expr_ref x = mk_skolem(symbol("seq.prefix.x"), e1, e2);
     expr_ref y = mk_skolem(symbol("seq.prefix.y"), e1, e2);
     expr_ref z = mk_skolem(symbol("seq.prefix.z"), e1, e2);
-    expr_ref c = mk_skolem(symbol("seq.prefix.c"), e1, e2, nullptr, char_sort);
-    expr_ref d = mk_skolem(symbol("seq.prefix.d"), e1, e2, nullptr, char_sort);
+    expr_ref c = mk_skolem(symbol("seq.prefix.c"), e1, e2, nullptr, nullptr, char_sort);
+    expr_ref d = mk_skolem(symbol("seq.prefix.d"), e1, e2, nullptr, nullptr, char_sort);
     add_axiom(lit, e2_is_emp, mk_seq_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y)));
     add_axiom(lit, e2_is_emp, mk_seq_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z)), mk_seq_eq(e2, x));
     add_axiom(lit, e2_is_emp, ~mk_eq(c, d, false), mk_seq_eq(e2, x));
@@ -4566,8 +5714,8 @@ void theory_seq::propagate_not_suffix(expr* e) {
     expr_ref x = mk_skolem(symbol("seq.suffix.x"), e1, e2);
     expr_ref y = mk_skolem(symbol("seq.suffix.y"), e1, e2);
     expr_ref z = mk_skolem(symbol("seq.suffix.z"), e1, e2);
-    expr_ref c = mk_skolem(symbol("seq.suffix.c"), e1, e2, nullptr, char_sort);
-    expr_ref d = mk_skolem(symbol("seq.suffix.d"), e1, e2, nullptr, char_sort);
+    expr_ref c = mk_skolem(symbol("seq.suffix.c"), e1, e2, nullptr, nullptr, char_sort);
+    expr_ref d = mk_skolem(symbol("seq.suffix.d"), e1, e2, nullptr, nullptr, char_sort);
     add_axiom(lit, e2_is_emp, mk_seq_eq(e1, mk_concat(y, m_util.str.mk_unit(c), x)));
     add_axiom(lit, e2_is_emp, mk_seq_eq(e2, mk_concat(z, m_util.str.mk_unit(d), x)), mk_seq_eq(e2, x));
     add_axiom(lit, e2_is_emp, ~mk_eq(c, d, false), mk_seq_eq(e2, x));
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 2f7cfd2b3..f32b6254b 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -29,6 +29,7 @@ Revision History:
 #include "math/automata/automaton.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "util/union_find.h"
+#include "util/obj_ref_hashtable.h"
 
 namespace smt {
 
@@ -48,6 +49,8 @@ namespace smt {
         typedef union_find<theory_seq> th_union_find;
 
         class seq_value_proc;
+        
+        theory_seq_params const & m_params;
 
         // cache to track evaluations under equalities
         class eval_cache {
@@ -301,6 +304,12 @@ namespace smt {
         unsigned                   m_eq_id;
         th_union_find              m_find;
 
+        obj_ref_map<ast_manager, expr, unsigned_vector>    m_overlap;
+        obj_ref_map<ast_manager, expr, unsigned_vector>    m_overlap2;
+        obj_map<enode, obj_map<enode, int>>   m_len_offset;
+        int                                   m_len_prop_lvl;
+
+
         seq_factory*               m_factory;    // value factory
         exclusion_table            m_exclude;    // set of asserted disequalities.
         expr_ref_vector            m_axioms;     // list of axioms to add.
@@ -321,7 +330,7 @@ namespace smt {
         stats            m_stats;
         symbol           m_prefix, m_suffix, m_accept, m_reject;
         symbol           m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
-        symbol           m_pre, m_post, m_eq;
+        symbol           m_pre, m_post, m_eq, m_seq_align;
         ptr_vector<expr> m_todo;
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
 
@@ -354,7 +363,7 @@ namespace smt {
         void pop_scope_eh(unsigned num_scopes) override;
         void restart_eh() override;
         void relevant_eh(app* n) override;
-        theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager()); }
+        theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); }
         char const * get_name() const override { return "seq"; }
         theory_var mk_var(enode* n) override;
         void apply_sort_cnstr(enode* n, sort* s) override;
@@ -366,23 +375,44 @@ namespace smt {
         void init_search_eh() override;
 
         void init_model(expr_ref_vector const& es);
+        
+        void len_offset(expr* const& e, rational val);
+        void prop_arith_to_len_offset();
+        int find_fst_non_empty_idx(expr_ref_vector const& x) const;
+        expr* find_fst_non_empty_var(expr_ref_vector const& x) const;
+        void find_max_eq_len(expr_ref_vector const& ls, expr_ref_vector const& rs);
+        bool has_len_offset(expr_ref_vector const& ls, expr_ref_vector const& rs, int & diff);
+        bool find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned const& idx, dependency*& deps, expr_ref_vector & res);
+        
         // final check 
         bool simplify_and_solve_eqs();   // solve unitary equalities
         bool reduce_length_eq();
         bool branch_unit_variable();     // branch on XYZ = abcdef
         bool branch_binary_variable();   // branch on abcX = Ydefg 
+        bool branch_ternary_variable1(); // branch on XabcY = Zdefg or XabcY = defgZ
+        bool branch_ternary_variable2(); // branch on XabcY = defgZmnpq
+        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
         bool branch_variable();          // branch on a variable
-        bool split_variable();           // split a variable
         bool is_solved(); 
         bool check_length_coherence();
         bool check_length_coherence0(expr* e);
         bool check_length_coherence(expr* e);
-        bool fixed_length();
-        bool fixed_length(expr* e);
+        bool fixed_length(bool is_zero = false);
+        bool fixed_length(expr* e, bool is_zero);
         void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
         bool branch_variable(eq const& e);
         bool branch_binary_variable(eq const& e);
+        bool eq_unit(expr* const& l, expr* const &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 indexes, expr* const& x, expr_ref_vector const& xs, expr* const& y1, expr_ref_vector const& ys, expr* const& y2);
+        bool 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);
+        bool branch_ternary_variable(eq const& e, bool flag1 = false);
+        bool branch_ternary_variable2(eq const& e, bool flag1 = false);
+        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);
         bool propagate_length_coherence(expr* e);  
         bool split_lengths(dependency* dep,
@@ -394,11 +424,14 @@ namespace smt {
         bool check_extensionality();
         bool check_contains();
         bool solve_eqs(unsigned start);
-        bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
+        bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep, unsigned idx);
         bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
         bool solve_unit_eq(expr* l, expr* r, dependency* dep);
         bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr*& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr*& y);
+        bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr*& x1, expr_ref_vector& xs, expr*& x2, expr*& y1, expr_ref_vector& ys, expr*& y2);
+        bool is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr*& x, expr_ref_vector& xs, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1);
+        bool is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& xs, expr*& x, expr*& y1, expr_ref_vector& ys, expr*& y2, bool flag1);
         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);
 
@@ -410,7 +443,7 @@ namespace smt {
         expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
         expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); }
         expr_ref mk_concat(expr_ref_vector const& es, sort* s) { if (es.empty()) return mk_empty(s); return mk_concat(es.size(), es.c_ptr()); }
-        expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty());  return mk_concat(es.size(), es.c_ptr()); }
+        expr* mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty());  return m_util.str.mk_concat(es.size(), es.c_ptr()); }
         expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr()); }
         expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); }
         expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); }
@@ -454,8 +487,9 @@ namespace smt {
         // variable solving utilities
         bool occurs(expr* a, expr* b);
         bool occurs(expr* a, expr_ref_vector const& b);
-        bool is_var(expr* b);
+        bool is_var(expr* b) const;
         bool add_solution(expr* l, expr* r, dependency* dep);
+        bool is_unit_nth(expr* a) const;
         bool is_nth(expr* a) const;
         bool is_nth(expr* a, expr*& e1, expr*& e2) const;
         bool is_tail(expr* a, expr*& s, unsigned& idx) const;
@@ -521,6 +555,7 @@ namespace smt {
         literal mk_seq_eq(expr* a, expr* b);
         void tightest_prefix(expr* s, expr* x);
         expr_ref mk_sub(expr* a, expr* b);
+        expr_ref mk_add(expr* a, expr* b);
         enode* ensure_enode(expr* a);
         
         dependency* mk_join(dependency* deps, literal lit);
@@ -530,11 +565,13 @@ namespace smt {
         // arithmetic integration
         bool get_num_value(expr* s, rational& val) const;
         bool lower_bound(expr* s, rational& lo) const;
+        bool lower_bound2(expr* s, rational& lo);
         bool upper_bound(expr* s, rational& hi) const;
         bool get_length(expr* s, rational& val) const;
 
         void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
-        expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, sort* range = nullptr);
+        expr* coalesce_chars(expr* const& str);
+        expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, expr* e4 = nullptr, sort* range = nullptr);
         bool is_skolem(symbol const& s, expr* e) const;
 
         void set_incomplete(app* term);
@@ -586,7 +623,7 @@ namespace smt {
         void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
         void display_nc(std::ostream& out, nc const& nc) const;
     public:
-        theory_seq(ast_manager& m);
+        theory_seq(ast_manager& m, theory_seq_params const & params);
         ~theory_seq() override;
 
         // model building
diff --git a/src/util/obj_ref_hashtable.h b/src/util/obj_ref_hashtable.h
index 3d6bbf883..23a2a1867 100644
--- a/src/util/obj_ref_hashtable.h
+++ b/src/util/obj_ref_hashtable.h
@@ -26,7 +26,7 @@ class obj_ref_map {
     M&                  m;
     obj_map<Key, Value> m_table;
 public:
-    typedef typename obj_map<Key, Value> iterator;
+    typedef typename obj_map<Key, Value>::iterator iterator;
     typedef Key key;
     typedef Value value;
     typedef typename obj_map<Key, Value>::key_data key_data;