diff --git a/.gitignore b/.gitignore
index 88ccbb56f..393c5a2a2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -73,6 +73,7 @@ src/api/ml/z3enums.ml
 src/api/ml/z3native.mli
 src/api/ml/z3enums.mli
 src/api/ml/z3.mllib
+out/**
 *.bak
 doc/api
 doc/code
diff --git a/README.md b/README.md
index 52b570246..0ecc17902 100644
--- a/README.md
+++ b/README.md
@@ -204,6 +204,9 @@ See [``examples/python``](examples/python) for examples.
 
 [WebAssembly](https://github.com/cpitclaudel/z3.wasm) bindings are provided by Clément Pit-Claudel.
 
+### ``Julia```
+Julia bindings can be enabled using the build option Z3_BUILD_JULIA_BINDINGS from the CMake system.
+
 ## System Overview
 
 ![System Diagram](https://github.com/Z3Prover/doc/blob/master/programmingz3/images/Z3Overall.jpg)
diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
index 590cfb438..c0d28a8ef 100644
--- a/src/ast/ast_ll_pp.cpp
+++ b/src/ast/ast_ll_pp.cpp
@@ -96,6 +96,10 @@ class ll_printer {
     void display_params(decl * d) {
         unsigned n = d->get_num_parameters();
         parameter const* p = d->get_parameters();
+        if (n > 0 && p[0].is_symbol() && d->get_name() == p[0].get_symbol()) {
+            n--;
+            p++;
+        } 
 
         if (n > 0 && !d->private_parameters()) {
             m_out << "[";
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index b1a70e2c4..5e9f66ece 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -519,7 +519,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         break;
     case OP_SEQ_INDEX:
         if (num_args == 2) {
-            expr_ref arg3(m_autil.mk_int(0), m());
+            expr_ref arg3(zero(), m());
             result = m_util.str.mk_index(args[0], args[1], arg3);
             st = BR_REWRITE1;
         }
@@ -689,9 +689,8 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
     // len(extract(s, offs, len(s) - offs)) = max(0, len(s) - offs)
     // 
     if (m_util.str.is_extract(a, s, offs, l) && is_suffix(s, offs, l)) {
-        expr_ref zero(m_autil.mk_int(0), m());
         result = m_autil.mk_sub(m_util.str.mk_length(s), offs);
-        result = m().mk_ite(m_autil.mk_ge(result, zero), result, zero);
+        result = m().mk_ite(m_autil.mk_ge(result, zero()), result, zero());
         return BR_REWRITE_FULL;
     }
 #endif
@@ -767,23 +766,24 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     bool constantPos = m_autil.is_numeral(b, pos);
     bool constantLen = m_autil.is_numeral(c, len);
     bool lengthPos   = m_util.str.is_length(b) || m_autil.is_add(b);
+    sort* a_sort = m().get_sort(a);
 
     sign sg;
     if (sign_is_determined(c, sg) && sg == sign_neg) {
-        result = m_util.str.mk_empty(m().get_sort(a));
+        result = m_util.str.mk_empty(a_sort);
         return BR_DONE;
     }
     
     // case 1: pos<0 or len<=0
     // rewrite to ""
     if ( (constantPos && pos.is_neg()) || (constantLen && !len.is_pos()) ) {
-        result = m_util.str.mk_empty(m().get_sort(a));
+        result = m_util.str.mk_empty(a_sort);
         return BR_DONE;
     }
     // case 1.1: pos >= length(base)
     // rewrite to ""
     if (constantPos && constantBase && pos >= rational(s.length())) {
-        result = m_util.str.mk_empty(m().get_sort(a));
+        result = m_util.str.mk_empty(a_sort);
         return BR_DONE;
     }
 
@@ -838,12 +838,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         }
         if (i == 0) return BR_FAILED;
         expr_ref t1(m()), t2(m());
-        if (m_lhs.size() == i) {
-            t1 = m_util.str.mk_empty(m().get_sort(a));
-        }
-        else {
-            t1 = m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i);
-        }
+        t1 = m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i, m().get_sort(a));        
         t2 = m_autil.mk_int(pos);
         for (expr* rhs : lens) {
             t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs));
@@ -897,11 +892,11 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         unsigned i = offset;
         for (; i < as.size() && m_util.str.is_unit(as.get(i)) && i - offset < _len; ++i);
         if (i - offset == _len) {
-            result = m_util.str.mk_concat(_len, as.c_ptr() + offset);
+            result = m_util.str.mk_concat(_len, as.c_ptr() + offset, m().get_sort(a));
             return BR_DONE;
         }
         if (i == as.size()) {
-            result = m_util.str.mk_concat(as.size() - offset, as.c_ptr() + offset);
+            result = m_util.str.mk_concat(as.size() - offset, as.c_ptr() + offset, m().get_sort(as.get(0)));
             return BR_DONE;
         }
     }
@@ -910,7 +905,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     }
     expr_ref pos1(m());
     pos1 = m_autil.mk_sub(b, m_autil.mk_int(offset));
-    result = m_util.str.mk_concat(as.size() - offset, as.c_ptr() + offset);
+    result = m_util.str.mk_concat(as.size() - offset, as.c_ptr() + offset, m().get_sort(as.get(0)));
     result = m_util.str.mk_substr(result, pos1, c);
     return BR_REWRITE3;
 }
@@ -1039,7 +1034,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
     }
     if (offs > 0 || sz < as.size()) {
         SASSERT(sz > offs);
-        result = m_util.str.mk_contains(m_util.str.mk_concat(sz-offs, as.c_ptr()+offs), b);
+        result = m_util.str.mk_contains(m_util.str.mk_concat(sz-offs, as.c_ptr()+offs, m().get_sort(a)), b);
         return BR_REWRITE2;
     }    
 
@@ -1078,18 +1073,19 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
     zstring c;
     rational r;
     expr_ref_vector lens(m());
+    sort* sort_a = m().get_sort(a);
     if (!get_lengths(b, lens, r)) {
         return BR_FAILED;
     }
     if (lens.empty() && r.is_neg()) {
-        result = m_util.str.mk_empty(m().get_sort(a));
+        result = m_util.str.mk_empty(sort_a);
         return BR_DONE;
     } 
 
     expr* a2 = nullptr, *i2 = nullptr;
     if (lens.empty() && m_util.str.is_at(a, a2, i2)) {
         if (r.is_pos()) {
-            result = m_util.str.mk_empty(m().get_sort(a));
+            result = m_util.str.mk_empty(sort_a);
         }
         else {
             result = a;
@@ -1126,14 +1122,14 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
         return BR_FAILED;
     }
     if (m_lhs.size() == i) {
-        result = m_util.str.mk_empty(m().get_sort(a));
+        result = m_util.str.mk_empty(sort_a);
         return BR_DONE;
     }
     expr_ref pos(m_autil.mk_int(r), m());
     for (expr* rhs : lens) {
         pos = m_autil.mk_add(pos, m_util.str.mk_length(rhs));
     }
-    result = m_util.str.mk_concat(m_lhs.size() - i , m_lhs.c_ptr() + i);
+    result = m_util.str.mk_concat(m_lhs.size() - i , m_lhs.c_ptr() + i, sort_a);
     result = m_util.str.mk_at(result, pos);
     return BR_REWRITE2;   
 }
@@ -1160,7 +1156,7 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
 
     expr* es[2] = { a, b};
     expr* la = m_util.str.mk_length(a);
-    result = m().mk_ite(m().mk_and(m_autil.mk_ge(b, m_autil.mk_int(0)), m().mk_not(m_autil.mk_le(la, b))), 
+    result = m().mk_ite(m().mk_and(m_autil.mk_ge(b, zero()), m().mk_not(m_autil.mk_le(la, b))), 
                         m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_I, 2, es), 
                         m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_U, 2, es));
     return BR_REWRITE_FULL;
@@ -1205,11 +1201,28 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 
+/**
+
+  Index of first occurrence of second string in first one starting at 
+  the position specified by the third argument.
+  (str.indexof s t i), with 0 <= i <= |s| is the position of the first
+  occurrence of t in s at or after position i, if any. 
+  Otherwise, it is -1. Note that the result is i whenever i is within
+  the range [0, |s|] and t is empty.
+  (str.indexof String String Int Int)
+
+   indexof(s, b, c) -> -1 if c < 0
+   indexof(a, "", 0) -> if a = "" then 0 else -1
+   indexof("", b, r) -> if b = "" and r = 0 then 0 else -1
+   indexof(unit(x)+a, b, r+1) -> indexof(a, b, r) 
+   indexof(unit(x)+a, unit(y)+b, 0) -> indexof(a,unit(y)+b, 0) if x != y
+*/
 br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) {
     zstring s1, s2;
     rational r;
     bool isc1 = m_util.str.is_string(a, s1);
     bool isc2 = m_util.str.is_string(b, s2);
+    sort* sort_a = m().get_sort(a);
 
     if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) {
         int idx = s1.indexofu(s2, r.get_unsigned());
@@ -1226,32 +1239,129 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
         return BR_DONE;
     }
 
+    
+    if (m_util.str.is_empty(a)) {
+        expr* emp = m_util.str.mk_is_empty(b);
+        result = m().mk_ite(m().mk_and(m().mk_eq(c, zero()), emp), zero(), minus_one());
+        return BR_REWRITE2;
+    }
+
     if (a == b) {
         if (m_autil.is_numeral(c, r)) {
-            if (r.is_zero()) {
-                result = m_autil.mk_int(0);
-            }
-            else {
-                result = m_autil.mk_int(-1);            
-            }
+            result = r.is_zero() ? zero() : minus_one();            
             return BR_DONE;
         }
         else {
-            result = m().mk_ite(m().mk_eq(m_autil.mk_int(0), c), m_autil.mk_int(0), m_autil.mk_int(-1));
+            result = m().mk_ite(m().mk_eq(zero(), c), zero(), minus_one());
             return BR_REWRITE2;
         }
     }
 
+    expr_ref_vector as(m()), bs(m());
+    m_util.str.get_concat_units(a, as);
+    unsigned i = 0;
+    if (m_autil.is_numeral(c, r)) {
+        i = 0;
+        while (r.is_pos() && m_util.str.is_unit(as.get(i))) {
+            r -= rational(1);
+            ++i;
+        }
+        if (i > 0) {
+            expr_ref a1(m());
+            a1 = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i, sort_a);
+            result = m_util.str.mk_index(a1, b, m_autil.mk_int(r));
+            return BR_REWRITE2;
+        }
+    }
+    bool is_zero = m_autil.is_numeral(c, r) && r.is_zero();
+    m_util.str.get_concat_units(b, bs);
+    i = 0;
+    while (is_zero && i < as.size() && 
+           0 < bs.size() && 
+           m_util.str.is_unit(as.get(i)) && 
+           m_util.str.is_unit(bs.get(0)) &&
+           m().are_distinct(as.get(i), bs.get(0))) {
+        ++i;
+    }
+    if (i > 0) {
+        result = m_util.str.mk_index(
+            m_util.str.mk_concat(as.size() - i, as.c_ptr() + i, sort_a), b, c);
+        return BR_REWRITE1;
+    }
+
+    switch (compare_lengths(as, bs)) {
+    case shorter_c:
+        if (is_zero) {
+            result = minus_one();
+            return BR_DONE;
+        }
+        break;
+    case same_length_c:
+        result = m().mk_ite(m_autil.mk_le(c, minus_one()), minus_one(), 
+                            m().mk_ite(m().mk_eq(c, zero()), 
+                                       m().mk_ite(m().mk_eq(a, b), zero(), minus_one()),
+                                       minus_one()));
+        return BR_REWRITE_FULL;
+    default:
+        break;
+    }
+    if (is_zero && !as.empty() && m_util.str.is_unit(as.get(0))) {
+        expr_ref a1(m_util.str.mk_concat(as.size() - 1, as.c_ptr() + 1, m().get_sort(as.get(0))), m());
+        expr_ref b1(m_util.str.mk_index(a1, b, c), m());
+        result = m().mk_ite(m_util.str.mk_prefix(b, a), zero(), 
+                            m().mk_ite(m_autil.mk_ge(b1, zero()), m_autil.mk_add(one(), b1), minus_one()));
+        return BR_REWRITE3;
+    }
     // Enhancement: walk segments of a, determine which segments must overlap, must not overlap, may overlap.
     return BR_FAILED;
 }
 
+seq_rewriter::length_comparison seq_rewriter::compare_lengths(unsigned sza, expr* const* as, unsigned szb, expr* const* bs) {
+    unsigned units_a = 0, units_b = 0, k = 0;
+    obj_map<expr, unsigned> mults;
+    bool b_has_foreign = false;
+    for (unsigned i = 0; i < sza; ++i) {
+        if (m_util.str.is_unit(as[i]))
+            units_a++;
+        else 
+            mults.insert_if_not_there2(as[i], 0)->get_data().m_value++;
+    }
+    for (unsigned i = 0; i < szb; ++i) {
+        if (m_util.str.is_unit(bs[i]))
+            units_b++;
+        else if (mults.find(bs[i], k)) {
+            --k;
+            if (k == 0) {
+                mults.erase(bs[i]);
+            }
+            else {
+                mults.insert(bs[i], k);
+            }
+        }
+        else {
+            b_has_foreign = true;
+        }
+    }
+    if (units_a > units_b && !b_has_foreign) {
+        return longer_c;
+    }
+    if (units_a == units_b && !b_has_foreign && mults.empty()) {
+        return same_length_c;
+    }
+    if (units_b > units_a && mults.empty()) {
+        return shorter_c;
+    }
+    return unknown_c;
+}
+
+
 //  (str.replace s t t') is the string obtained by replacing the first occurrence 
 //  of t in s, if any, by t'. Note that if t is empty, the result is to prepend
 //  t' to s; also, if t does not occur in s then the result is s.
 
 br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result) {
     zstring s1, s2, s3;
+    sort* sort_a = m().get_sort(a);
     if (m_util.str.is_string(a, s1) && m_util.str.is_string(b, s2) && 
         m_util.str.is_string(c, s3)) {
         result = m_util.str.mk_string(s1.replace(s2, s3));
@@ -1288,7 +1398,7 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
     // a := b + rest
     if (m_lhs.get(0) == b) {
         m_lhs[0] = c;
-        result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr());
+        result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr(), sort_a);
         return BR_REWRITE1;
     }
 
@@ -1296,7 +1406,7 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
     if (m_util.str.is_string(b, s2) && m_util.str.is_string(c, s3) && 
         m_util.str.is_string(m_lhs.get(0), s1) && s1.contains(s2) ) {
         m_lhs[0] = m_util.str.mk_string(s1.replace(s2, s3));
-        result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr());
+        result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr(), sort_a);
         return BR_REWRITE1;
     }
 
@@ -1308,6 +1418,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     zstring s1, s2;
     bool isc1 = m_util.str.is_string(a, s1);
     bool isc2 = m_util.str.is_string(b, s2);
+    sort* sort_a = m().get_sort(a);
     if (isc1 && isc2) {
         result = m().mk_bool_val(s1.prefixof(s2));
         TRACE("seq", tout << result << "\n";);
@@ -1336,8 +1447,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
                 SASSERT(as.size() > 1);
                 s2 = s2.extract(s1.length(), s2.length()-s1.length());
                 bs[0] = m_util.str.mk_string(s2);
-                result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1),
-                                              m_util.str.mk_concat(bs.size(), bs.c_ptr()));
+                result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1, sort_a),
+                                              m_util.str.mk_concat(bs.size(), bs.c_ptr(), sort_a));
                 TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
                 return BR_REWRITE_FULL;
             }
@@ -1359,8 +1470,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
                 SASSERT(bs.size() > 1);
                 s1 = s1.extract(s2.length(), s1.length() - s2.length());
                 as[0] = m_util.str.mk_string(s1);
-                result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()),
-                                     m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1));
+                result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr(), sort_a),
+                                              m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1, sort_a));
                 TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
                 return BR_REWRITE_FULL;                
             }
@@ -1406,8 +1517,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     }
     if (i > 0) {
         SASSERT(i < as.size() && i < bs.size());
-        a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
-        b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i); 
+        a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i, sort_a);
+        b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i, sort_a); 
         eqs.push_back(m_util.str.mk_prefix(a, b));
         result = mk_and(eqs);
         TRACE("seq", tout << result << "\n";);
@@ -1423,6 +1534,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
         return BR_DONE;
     }
     zstring s1, s2;
+    sort* sort_a = m().get_sort(a);
     if (m_util.str.is_empty(a)) {
         result = m().mk_true();
         return BR_DONE;
@@ -1431,69 +1543,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
         result = m_util.str.mk_is_empty(a);
         return BR_REWRITE3;
     }
-
-    bool isc1 = false;
-    bool isc2 = false;
-    expr *a1 = nullptr, *a2 = nullptr, *b1 = nullptr, *b2 = nullptr;
-    if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
-        isc1 = true;
-    }
-    else if (m_util.str.is_string(a, s1)) {
-        isc1 = true;
-        a2 = a;
-        a1 = nullptr;
-    }
-
-    if (m_util.str.is_concat(b, b1, b2) && m_util.str.is_string(b2, s2)) {
-        isc2 = true;
-    }
-    else if (m_util.str.is_string(b, s2)) {
-        isc2 = true;
-        b2 = b;
-        b1 = nullptr;
-    }
-    if (isc1 && isc2) {
-        if (s1.length() == s2.length()) {
-            //SASSERT(s1 != s2);
-            result = m().mk_false();
-            return BR_DONE;
-        }
-        else if (s1.length() < s2.length()) {
-            bool suffix = s1.suffixof(s2);
-            if (suffix && a1 == nullptr) {
-                result = m().mk_true();
-                return BR_DONE;
-            }
-            else if (suffix) {
-                s2 = s2.extract(0, s2.length()-s1.length());
-                b2 = m_util.str.mk_string(s2);
-                result = m_util.str.mk_suffix(a1, b1?m_util.str.mk_concat(b1, b2):b2);
-                return BR_DONE;
-            }
-            else {
-                result = m().mk_false();
-                return BR_DONE;
-            }
-        }
-        else {
-            SASSERT(s1.length() > s2.length());
-            if (b1 == nullptr) {
-                result = m().mk_false();
-                return BR_DONE;
-            }
-            bool suffix = s2.suffixof(s1);
-            if (suffix) {
-                s1 = s1.extract(0, s1.length()-s2.length());
-                a2 = m_util.str.mk_string(s1);
-                result = m_util.str.mk_suffix(a1?m_util.str.mk_concat(a1, a2):a2, b1);
-                return BR_DONE;
-            }
-            else {
-                result = m().mk_false();
-                return BR_DONE;
-            }            
-        }
-    }
+    
     expr_ref_vector as(m()), bs(m()), eqs(m());
     m_util.str.get_concat_units(a, as);
     m_util.str.get_concat_units(b, bs);
@@ -1530,8 +1580,8 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
 
     if (i > 1) {
         SASSERT(i <= sza && i <= szb);
-        a = m_util.str.mk_concat(sza - i + 1, as.c_ptr());
-        b = m_util.str.mk_concat(szb - i + 1, bs.c_ptr());
+        a = m_util.str.mk_concat(sza - i + 1, as.c_ptr(), sort_a);
+        b = m_util.str.mk_concat(szb - i + 1, bs.c_ptr(), sort_a);
         eqs.push_back(m_util.str.mk_suffix(a, b));
         result = mk_and(eqs);
         TRACE("seq", tout << result << "\n";);
@@ -1549,12 +1599,7 @@ br_status seq_rewriter::mk_str_units(func_decl* f, expr_ref& result) {
     for (unsigned j = 0; j < sz; ++j) {
         es.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, j)));
     }        
-    if (es.empty()) {
-        result = m_util.str.mk_empty(f->get_range());
-    }
-    else {
-        result = m_util.str.mk_concat(es);
-    }
+    result = m_util.str.mk_concat(es, f->get_range());    
     return BR_DONE;
 }
 
@@ -1612,12 +1657,12 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
     if (m_util.str.is_string(a, str)) {
         std::string s = str.encode();
         if (s.length() == 0) {
-            result = m_autil.mk_int(-1);
+            result = minus_one();
             return BR_DONE;
         } 
         for (unsigned i = 0; i < s.length(); ++i) {
             if (!('0' <= s[i] && s[i] <= '9')) {
-                result = m_autil.mk_int(-1);
+                result = minus_one();
                 return BR_DONE;
             }
         }
@@ -1627,7 +1672,7 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
     }
     expr* b;
     if (m_util.str.is_itos(a, b)) {
-        result = m().mk_ite(m_autil.mk_ge(b, m_autil.mk_int(0)), b, m_autil.mk_int(-1));
+        result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one());
         return BR_DONE;
     }
     return BR_FAILED;
@@ -1740,12 +1785,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
     if (is_sequence(*aut, seq)) {
         TRACE("seq", tout << seq << "\n";);
               
-        if (seq.empty()) {
-            result = m_util.str.mk_is_empty(a);
-        }
-        else {
-            result = m().mk_eq(a, m_util.str.mk_concat(seq));
-        }
+        result = m().mk_eq(a, m_util.str.mk_concat(seq, m().get_sort(a)));        
         return BR_REWRITE3;
     }
 
@@ -2152,9 +2192,10 @@ br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
 
 br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
     TRACE("seq", tout << mk_bounded_pp(l, m(), 2) << " = " << mk_bounded_pp(r, m(), 2) << "\n";);
-    expr_ref_vector lhs(m()), rhs(m()), res(m());
+    expr_ref_vector res(m());
+    expr_ref_pair_vector new_eqs(m());
     bool changed = false;
-    if (!reduce_eq(l, r, lhs, rhs, changed)) {
+    if (!reduce_eq(l, r, new_eqs, changed)) {
         result = m().mk_false();
         TRACE("seq", tout << result << "\n";);
         return BR_DONE;
@@ -2162,19 +2203,19 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
     if (!changed) {
         return BR_FAILED;
     }
-    for (unsigned i = 0; i < lhs.size(); ++i) {
-        res.push_back(m().mk_eq(lhs.get(i), rhs.get(i)));
+    for (auto const& p : new_eqs) {
+        res.push_back(m().mk_eq(p.first, p.second));
     }
     result = mk_and(res);
     TRACE("seq", tout << result << "\n";);
     return BR_REWRITE3;
 }
 
-bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
-    expr* a, *b;
+bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs, bool& change) {
+    expr* a, *b;    
     zstring s;
     bool lchange = false;
-    SASSERT(lhs.empty());
+    SASSERT(new_eqs.empty());
     TRACE("seq_verbose", tout << ls << "\n"; tout << rs << "\n";);
     // solve from back
     while (true) {
@@ -2202,8 +2243,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
             if (m().are_distinct(a, b)) {
                 return false;
             }
-            lhs.push_back(a);
-            rhs.push_back(b);
+            new_eqs.push_back(a, b);
             ls.pop_back();
             rs.pop_back();
         }
@@ -2212,8 +2252,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
             
             app* ch = m_util.str.mk_char(s, s.length()-1);
             SASSERT(m().get_sort(ch) == m().get_sort(a));
-            lhs.push_back(ch);
-            rhs.push_back(a);
+            new_eqs.push_back(ch, a);
             ls.pop_back();
             if (s.length() == 1) {
                 rs.pop_back();
@@ -2260,8 +2299,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
             if (m().are_distinct(a, b)) {
                 return false;
             }
-            lhs.push_back(a);
-            rhs.push_back(b);
+            new_eqs.push_back(a, b);
             ++head1;
             ++head2;
         }
@@ -2269,8 +2307,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
             SASSERT(s.length() > 0);
             app* ch = m_util.str.mk_char(s, 0);
             SASSERT(m().get_sort(ch) == m().get_sort(a));
-            lhs.push_back(ch);
-            rhs.push_back(a);
+            new_eqs.push_back(ch, a);
             ++head1;
             if (s.length() == 1) {
                 ++head2;
@@ -2345,13 +2382,13 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
     unsigned szl = ls.size() - head1, szr = rs.size() - head2;
     expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2;
 
-    if (solve_itos(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
+    if (solve_itos(szl, _ls, szr, _rs, new_eqs, is_sat)) {
         ls.reset(); rs.reset();
         change = true;
         return is_sat;
     }
 
-    if (length_constrained(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
+    if (length_constrained(szl, _ls, szr, _rs, new_eqs, is_sat)) {
         ls.reset(); rs.reset();
         change = true;
         return is_sat;
@@ -2367,12 +2404,11 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
         std::swap(_ls, _rs);
     }
     if (szl == 0 && szr > 0) {
-        if (set_empty(szr, _rs, true, lhs, rhs)) {
+        if (set_empty(szr, _rs, true, new_eqs)) {
             lchange |= szr > 1; 
             change  |= szr > 1;
             if (szr == 1 && !lchange) {
-                lhs.reset();
-                rhs.reset();
+                new_eqs.reset();
             }
             else {
                 ls.reset();        
@@ -2386,7 +2422,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
     }
     SASSERT(szl > 0 && szr > 0);
 
-    if (is_subsequence(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
+    if (is_subsequence(szl, _ls, szr, _rs, new_eqs, is_sat)) {
         ls.reset(); rs.reset();
         change = true;
         return is_sat;
@@ -2411,36 +2447,26 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
     return true;
 }
 
-void seq_rewriter::add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs) {
-    if (ls.empty() && !rs.empty()) {
-        rhs.push_back(m_util.str.mk_concat(rs));
-        lhs.push_back(m_util.str.mk_empty(m().get_sort(rhs.back())));
-    }
-    else if (rs.empty() && !ls.empty()) {
-        lhs.push_back(m_util.str.mk_concat(ls));
-        rhs.push_back(m_util.str.mk_empty(m().get_sort(lhs.back())));
-    }
-    else if (!rs.empty() && !ls.empty()) {
-        lhs.push_back(m_util.str.mk_concat(ls));
-        rhs.push_back(m_util.str.mk_concat(rs));
+void seq_rewriter::add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& eqs) {
+    if (!ls.empty() || !rs.empty()) {
+        sort * s = m().get_sort(ls.empty() ? rs[0] : ls[0]);
+        eqs.push_back(m_util.str.mk_concat(ls, s), m_util.str.mk_concat(rs, s));
     }
 }
 
 
-bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& changed) {
+bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_pair_vector& new_eqs, bool& changed) {
     m_lhs.reset();
     m_rhs.reset();
     m_util.str.get_concat(l, m_lhs);
     m_util.str.get_concat(r, m_rhs);
     bool change = false;
-    if (reduce_eq(m_lhs, m_rhs, lhs, rhs, change)) {
-        SASSERT(lhs.size() == rhs.size());
+    if (reduce_eq(m_lhs, m_rhs, new_eqs, change)) {
         if (!change) {
-            lhs.push_back(l);
-            rhs.push_back(r);
+            new_eqs.push_back(std::make_pair(l, r));
         }
         else {
-            add_seqs(m_lhs, m_rhs, lhs, rhs);
+            add_seqs(m_lhs, m_rhs, new_eqs);
         }
         changed |= change;
         return true;
@@ -2455,6 +2481,7 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) {
     m_lhs.reset();
     m_util.str.get_concat(a, m_lhs);
     TRACE("seq", tout << expr_ref(a, m()) << " " << expr_ref(b, m()) << "\n";);
+    sort* sort_a = m().get_sort(a);
     zstring s;
     for (unsigned i = 0; i < m_lhs.size(); ++i) {
         expr* e = m_lhs.get(i);
@@ -2470,18 +2497,18 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) {
             }
             es.append(m_lhs.size() - i, m_lhs.c_ptr() + i);
             for (unsigned j = 0; j < sz; ++j) {
-                disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(es.size() - j, es.c_ptr() + j)));
+                disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(es.size() - j, es.c_ptr() + j, sort_a)));
             }
             continue;
         }
         if (m_util.str.is_unit(e)) {
-            disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i)));
+            disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i, sort_a)));
             continue;
         }
 
         if (m_util.str.is_string(b, s)) {
             expr* all = m_util.re.mk_full_seq(m_util.re.mk_re(m().get_sort(b)));
-            disj.push_back(m_util.re.mk_in_re(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i),
+            disj.push_back(m_util.re.mk_in_re(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i, sort_a),
                                               m_util.re.mk_concat(all, m_util.re.mk_concat(m_util.re.mk_to_re(b), all))));
             return true;
         }
@@ -2489,7 +2516,7 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) {
         if (i == 0) {
             return false;
         }
-        disj.push_back(m_util.str.mk_contains(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i), b));
+        disj.push_back(m_util.str.mk_contains(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i, sort_a), b));
         return true;
     }
     disj.push_back(m_util.str.mk_is_empty(b));
@@ -2506,15 +2533,10 @@ expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
             bs.push_back(as[i]);
         }
     }    
-    if (bs.empty()) {
-        return m_util.str.mk_empty(m().get_sort(as[0]));
-    }
-    else {
-        return m_util.str.mk_concat(bs.size(), bs.c_ptr());
-    }
+    return m_util.str.mk_concat(bs.size(), bs.c_ptr(), m().get_sort(as[0]));    
 }
 
-bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs) {
+bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_pair_vector& eqs) {
     zstring s;
     expr* emp = nullptr;
     for (unsigned i = 0; i < sz; ++i) {
@@ -2532,8 +2554,7 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_ve
         }
         else {
             emp = emp?emp:m_util.str.mk_empty(m().get_sort(es[i]));
-            lhs.push_back(emp);
-            rhs.push_back(es[i]);
+            eqs.push_back(emp, es[i]);
         }
     }
     return true;
@@ -2579,15 +2600,15 @@ bool seq_rewriter::is_string(unsigned n, expr* const* es, zstring& s) const {
 }
 
 bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs, 
-                              expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
+                              expr_ref_pair_vector& eqs, bool& is_sat) {
     expr* n = nullptr;
     is_sat = true;
     if (szl == 1 && m_util.str.is_itos(ls[0], n) &&
-        solve_itos(n, szr, rs, lhs, rhs)) {
+        solve_itos(n, szr, rs, eqs)) {
         return true;
     }
     if (szr == 1 && m_util.str.is_itos(rs[0], n) &&
-        solve_itos(n, szl, ls, rhs, lhs)) {
+        solve_itos(n, szl, ls, eqs)) {
         return true;
     }
     return false;
@@ -2597,14 +2618,13 @@ bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr*
  * itos(n) = <numeric string> -> n = numeric
  */
 
-bool seq_rewriter::solve_itos(expr* n, unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs) {
+bool seq_rewriter::solve_itos(expr* n, unsigned sz, expr* const* es, expr_ref_pair_vector& eqs) {
     zstring s;
     if (is_string(sz, es, s)) {
         std::string s1 = s.encode();
         rational r(s1.c_str());
         if (s1 == r.to_string()) {
-            lhs.push_back(n);
-            rhs.push_back(m_autil.mk_numeral(r, true));
+            eqs.push_back(n, m_autil.mk_numeral(r, true));
             return true;
         }
     }        
@@ -2612,7 +2632,7 @@ bool seq_rewriter::solve_itos(expr* n, unsigned sz, expr* const* es, expr_ref_ve
 }
 
 bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr, expr* const* r, 
-                                      expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
+                                      expr_ref_pair_vector& eqs, bool& is_sat) {
     is_sat = true;
     unsigned len1 = 0, len2 = 0;
     bool bounded1 = min_length(szl, l, len1);
@@ -2626,44 +2646,39 @@ bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr
         return true;
     }
     if (bounded1 && len1 == len2 && len1 > 0) {
-        is_sat = set_empty(szr, r, false, lhs, rhs);
+        is_sat = set_empty(szr, r, false, eqs);
         if (is_sat) {
-            lhs.push_back(concat_non_empty(szl, l));
-            rhs.push_back(concat_non_empty(szr, r));
-            //split_units(lhs, rhs);
+            eqs.push_back(concat_non_empty(szl, l), concat_non_empty(szr, r));
+            //split_units(eqs);
         }
         return true;
     }
     if (bounded2 && len1 == len2 && len1 > 0) {
-        is_sat = set_empty(szl, l, false, lhs, rhs);
         if (is_sat) {
-            lhs.push_back(concat_non_empty(szl, l));
-            rhs.push_back(concat_non_empty(szr, r));
-            //split_units(lhs, rhs);
+            eqs.push_back(concat_non_empty(szl, l), concat_non_empty(szr, r));
+            //split_units(eqs);
         }
         return true;
     }    
     return false;
 }
 
-void seq_rewriter::split_units(expr_ref_vector& lhs, expr_ref_vector& rhs) {
+void seq_rewriter::split_units(expr_ref_pair_vector& eqs) {
     expr* a, *b, *a1, *b1, *a2, *b2;
-    while (true) {
-        if (m_util.str.is_unit(lhs.back(), a) &&
-            m_util.str.is_unit(rhs.back(), b)) {
-            lhs[lhs.size()-1] = a;
-            rhs[rhs.size()-1] = b;
+    while (!eqs.empty()) {
+        auto const& p = eqs.back();
+        if (m_util.str.is_unit(p.first, a) &&
+            m_util.str.is_unit(p.second, b)) {
+            eqs[eqs.size()-1] = std::make_pair(a, b);
             break;
         }
-        if (m_util.str.is_concat(lhs.back(), a, a2) && 
+        if (m_util.str.is_concat(p.first, a, a2) && 
             m_util.str.is_unit(a, a1) && 
-            m_util.str.is_concat(rhs.back(), b, b2) &&
+            m_util.str.is_concat(p.second, b, b2) &&
             m_util.str.is_unit(b, b1)) {
-            expr_ref _pin_a(lhs.back(), m()), _pin_b(rhs.back(), m());
-            lhs[lhs.size()-1] = a1;
-            rhs[rhs.size()-1] = b1;
-            lhs.push_back(a2);
-            rhs.push_back(b2);
+            expr_ref _pin_a(p.first, m()), _pin_b(p.second, m());
+            eqs[eqs.size()-1] = std::make_pair(a1, b1);
+            eqs.push_back(a2, b2);
         }
         else {
             break;
@@ -2679,7 +2694,7 @@ bool seq_rewriter::is_epsilon(expr* e) const {
 }
 
 bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, expr* const* r, 
-                                  expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
+                                  expr_ref_pair_vector& eqs, bool& is_sat) {
     is_sat = true;
     if (szl == szr) return false;
     if (szr < szl) {
@@ -2710,7 +2725,7 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex
         if (rpos.contains(j)) {
             rs.push_back(r[j]);
         }
-        else if (!set_empty(1, r + j, true, lhs, rhs)) {
+        else if (!set_empty(1, r + j, true, eqs)) {
             is_sat = false;
             return true;
         }
@@ -2723,8 +2738,9 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex
     }
     SASSERT(szl == rs.size());
     if (szl > 0) {
-        lhs.push_back(m_util.str.mk_concat(szl, l));
-        rhs.push_back(m_util.str.mk_concat(szl, rs.c_ptr()));
+        sort* srt = m().get_sort(l[0]);
+        eqs.push_back(m_util.str.mk_concat(szl, l, srt),
+                      m_util.str.mk_concat(szl, rs.c_ptr(), srt));
     }
     return true;
 } 
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 0154a93d5..4f3da3cd4 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -22,12 +22,15 @@ Notes:
 #include "ast/seq_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/rewriter_types.h"
+#include "util/ref_pair_vector.h"
 #include "util/params.h"
 #include "util/lbool.h"
 #include "util/sign.h"
 #include "math/automata/automaton.h"
 #include "math/automata/symbolic_automata.h"
 
+typedef ref_pair_vector<expr, ast_manager> expr_ref_pair_vector;
+
 class sym_expr {
     enum ty {
         t_char,
@@ -111,6 +114,18 @@ class seq_rewriter {
     expr_ref_vector m_es, m_lhs, m_rhs;
     bool           m_coalesce_chars;
 
+    enum length_comparison {
+        shorter_c, 
+        longer_c,
+        same_length_c,
+        unknown_c
+    };
+
+    length_comparison compare_lengths(expr_ref_vector const& as, expr_ref_vector const& bs) {
+        return compare_lengths(as.size(), as.c_ptr(), bs.size(), bs.c_ptr());
+    }
+    length_comparison compare_lengths(unsigned sza, expr* const* as, unsigned szb, expr* const* bs);
+
     br_status mk_seq_unit(expr* e, expr_ref& result);
     br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_length(expr* a, expr_ref& result);
@@ -143,18 +158,21 @@ class seq_rewriter {
 
     bool cannot_contain_prefix(expr* a, expr* b);
     bool cannot_contain_suffix(expr* a, expr* b);
+    expr_ref zero() { return expr_ref(m_autil.mk_int(0), m()); }
+    expr_ref one() { return expr_ref(m_autil.mk_int(1), m()); }
+    expr_ref minus_one() { return expr_ref(m_autil.mk_int(-1), m()); }
 
     bool is_suffix(expr* s, expr* offset, expr* len);
     bool sign_is_determined(expr* len, sign& s);
 
-    bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
+    bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_pair_vector& eqs);
     bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, 
-                        expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
+                        expr_ref_pair_vector& eqs, bool& is_sat);
     bool length_constrained(unsigned n, expr* const* l, unsigned m, expr* const* r, 
-                        expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
+                        expr_ref_pair_vector& eqs, bool& is_sat);
     bool solve_itos(unsigned n, expr* const* l, unsigned m, expr* const* r, 
-                    expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
-    bool solve_itos(expr* n, unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs);
+                    expr_ref_pair_vector& eqs, bool& is_sat);
+    bool solve_itos(expr* n, unsigned sz, expr* const* es, expr_ref_pair_vector& eqs);
     bool min_length(unsigned n, expr* const* es, unsigned& len);
     expr* concat_non_empty(unsigned n, expr* const* es);
 
@@ -164,7 +182,7 @@ class seq_rewriter {
     bool is_sequence(expr* e, expr_ref_vector& seq);
     bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
     bool is_epsilon(expr* e) const;
-    void split_units(expr_ref_vector& lhs, expr_ref_vector& rhs);
+    void split_units(expr_ref_pair_vector& eqs);
     bool get_lengths(expr* e, expr_ref_vector& lens, rational& pos);
 
 
@@ -186,13 +204,13 @@ public:
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
 
-    bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);
+    bool reduce_eq(expr* l, expr* r, expr_ref_pair_vector& new_eqs, bool& change);
 
-    bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);
+    bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs, bool& change);
 
     bool reduce_contains(expr* a, expr* b, expr_ref_vector& disj);
 
-    void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs);
+    void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs);
 
 
 };
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 19db86ca3..7fb119951 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -264,8 +264,11 @@ public:
         app* mk_char(char ch) const;
         app* mk_concat(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
         app* mk_concat(expr* a, expr* b, expr* c) const { return mk_concat(a, mk_concat(b, c)); }
-        expr* mk_concat(unsigned n, expr* const* es) const { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
-        expr* mk_concat(expr_ref_vector const& es) const { return mk_concat(es.size(), es.c_ptr()); }
+        expr* mk_concat(unsigned n, expr* const* es, sort* s) const { 
+            if (n == 0) return mk_empty(s);
+            if (n == 1) return es[0]; 
+            return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
+        expr* mk_concat(expr_ref_vector const& es, sort* s) const { return mk_concat(es.size(), es.c_ptr(), s); }
         app* mk_length(expr* a) const { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
         app* mk_at(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_AT, 2, es); }
         app* mk_nth(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_NTH, 2, es); }
diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h
index 4edbb2b9d..96b2dd03c 100644
--- a/src/math/simplex/sparse_matrix.h
+++ b/src/math/simplex/sparse_matrix.h
@@ -140,6 +140,7 @@ namespace simplex {
         bool well_formed_row(unsigned row_id) const;
         bool well_formed_column(unsigned column_id) const;
         void del_row_entry(_row& r, unsigned pos);
+        void reset_rows();
 
     public:
 
diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h
index c68116190..512b4ec8c 100644
--- a/src/math/simplex/sparse_matrix_def.h
+++ b/src/math/simplex/sparse_matrix_def.h
@@ -40,8 +40,8 @@ namespace simplex {
 
     template<typename Ext>
     void sparse_matrix<Ext>::_row::reset(manager& m) {
-        for (unsigned i = 0; i < m_entries.size(); ++i) {
-            m.reset(m_entries[i].m_coeff);
+        for (auto & e : m_entries) {
+            m.reset(e.m_coeff);
         }
         m_entries.reset();
         m_size           = 0;
@@ -135,25 +135,25 @@ namespace simplex {
     */
     template<typename Ext>
     inline void sparse_matrix<Ext>::_row::save_var_pos(svector<int> & result_map, unsigned_vector& idxs) const {
-        typename vector<_row_entry>::const_iterator it  = m_entries.begin();
-        typename vector<_row_entry>::const_iterator end = m_entries.end();
+
         unsigned idx = 0;
-        for (; it != end; ++it, ++idx) {
-            if (!it->is_dead()) {
-                result_map[it->m_var] = idx;
-                idxs.push_back(it->m_var);
+        for (auto const& e : m_entries) {
+            if (!e.is_dead()) {
+                result_map[e.m_var] = idx;
+                idxs.push_back(e.m_var);
             }
+            ++idx;
         }
     }
 
 
     template<typename Ext>
     int sparse_matrix<Ext>::_row::get_idx_of(var_t v) const {
-        typename vector<_row_entry>::const_iterator it  = m_entries.begin();
-        typename vector<_row_entry>::const_iterator end = m_entries.end();
-        for (unsigned idx = 0; it != end; ++it, ++idx) {
-            if (!it->is_dead() && it->m_var == v)
+        unsigned idx = 0; 
+        for (auto const& e : m_entries) {
+            if (!e.is_dead() && e.m_var == v)
                 return idx;
+            ++idx;
         }
         return -1;
     }
@@ -205,32 +205,12 @@ namespace simplex {
         }
     }
 
-#if 0
-    /**
-       \brief Special version of compress, that is used when the column contain
-       only one entry located at position singleton_pos.
-    */
-    template<typename Ext>
-    void sparse_matrix<Ext>::column::compress_singleton(vector<_row> & rows, unsigned singleton_pos) {
-        SASSERT(m_size == 1);
-        if (singleton_pos != 0) {
-            col_entry & s  = m_entries[singleton_pos];
-            m_entries[0]   = s;
-            row & r        = rows[s.m_row_id];
-            r[s.m_row_idx].m_col_idx = 0;
-        }
-        m_first_free_idx = -1;
-        m_entries.shrink(1);
-    }
-#endif
     template<typename Ext>
     const typename sparse_matrix<Ext>::col_entry * 
     sparse_matrix<Ext>::column::get_first_col_entry() const {
-        typename svector<col_entry>::const_iterator it  = m_entries.begin();
-        typename svector<col_entry>::const_iterator end = m_entries.end();
-        for (; it != end; ++it) {
-            if (!it->is_dead()) {
-                return it;
+        for (auto const& e : m_entries) {
+            if (!e.is_dead()) {
+                return &e;
             }
         }
         return nullptr;
@@ -272,16 +252,21 @@ namespace simplex {
 
     template<typename Ext>
     sparse_matrix<Ext>::~sparse_matrix() {
-        for (unsigned i = 0; i < m_rows.size(); ++i) {
-            _row& r = m_rows[i];
-            for (unsigned j = 0; j < r.m_entries.size(); ++j) {
-                m.reset(r.m_entries[j].m_coeff);
+        reset_rows();
+    }
+
+    template<typename Ext>
+    void sparse_matrix<Ext>::reset_rows() {
+        for (auto& r : m_rows) {
+            for (auto& e : r.m_entries) {
+                m.reset(e.m_coeff);
             }
         }
     }
 
     template<typename Ext>
     void sparse_matrix<Ext>::reset() {
+        reset_rows();
         m_rows.reset();
         m_dead_rows.reset();
         m_columns.reset();
diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt
index a3f46e54c..6e79bbab8 100644
--- a/src/sat/CMakeLists.txt
+++ b/src/sat/CMakeLists.txt
@@ -33,7 +33,6 @@ z3_add_component(sat
     sat_scc.cpp
     sat_simplifier.cpp
     sat_solver.cpp
-    sat_unit_walk.cpp
     sat_watched.cpp
     sat_xor_finder.cpp
   COMPONENT_DEPENDENCIES
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 6819da579..2905d334c 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1865,7 +1865,7 @@ namespace sat {
     }
 
     ba_solver::ba_solver()
-        : m_solver(nullptr), m_lookahead(nullptr), m_unit_walk(nullptr), 
+        : m_solver(nullptr), m_lookahead(nullptr), 
           m_constraint_id(0), m_ba(*this), m_sort(m_ba) {
         TRACE("ba", tout << this << "\n";);
         m_num_propagations_since_pop = 0;
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index 50f12fe71..b99cb945f 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -24,7 +24,6 @@ Revision History:
 #include "sat/sat_extension.h"
 #include "sat/sat_solver.h"
 #include "sat/sat_lookahead.h"
-#include "sat/sat_unit_walk.h"
 #include "sat/sat_big.h"
 #include "util/small_object_allocator.h"
 #include "util/scoped_ptr_vector.h"
@@ -230,7 +229,6 @@ namespace sat {
 
         solver*                m_solver;
         lookahead*             m_lookahead;
-        unit_walk*             m_unit_walk;
         stats                  m_stats; 
         small_object_allocator m_allocator;
        
@@ -445,23 +443,20 @@ namespace sat {
         inline lbool value(model const& m, literal l) const { return l.sign() ? ~m[l.var()] : m[l.var()]; }
         inline bool is_false(literal lit) const { return l_false == value(lit); }
 
-        inline unsigned lvl(literal lit) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(lit); }
-        inline unsigned lvl(bool_var v) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(v); }
+        inline unsigned lvl(literal lit) const { return m_lookahead ? 0 : m_solver->lvl(lit); }
+        inline unsigned lvl(bool_var v) const { return m_lookahead ? 0 : m_solver->lvl(v); }
         inline bool inconsistent() const { 
             if (m_lookahead) return m_lookahead->inconsistent(); 
-            if (m_unit_walk) return m_unit_walk->inconsistent();
             return m_solver->inconsistent(); 
         }
         inline watch_list& get_wlist(literal l) { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
         inline watch_list const& get_wlist(literal l) const { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
         inline void assign(literal l, justification j) { 
             if (m_lookahead) m_lookahead->assign(l); 
-            else if (m_unit_walk) m_unit_walk->assign(l);
             else m_solver->assign(l, j);
         }
         inline void set_conflict(justification j, literal l) { 
             if (m_lookahead) m_lookahead->set_conflict(); 
-            else if (m_unit_walk) m_unit_walk->set_conflict();
             else m_solver->set_conflict(j, l); 
         }
         inline config const& get_config() const { return m_lookahead ? m_lookahead->get_config() : m_solver->get_config(); }
@@ -544,7 +539,6 @@ namespace sat {
         ~ba_solver() override;
         void set_solver(solver* s) override { m_solver = s; }
         void set_lookahead(lookahead* l) override { m_lookahead = l; }
-        void set_unit_walk(unit_walk* u) override { m_unit_walk = u; }
         void    add_at_least(bool_var v, literal_vector const& lits, unsigned k);
         void    add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
         void    add_xr(literal_vector const& lits);
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 744608fa8..388fd56f3 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -98,8 +98,6 @@ namespace sat {
         else
             m_local_search_mode = local_search_mode::wsat;
         m_local_search_dbg_flips = p.local_search_dbg_flips();
-        m_unit_walk       = p.unit_walk();
-        m_unit_walk_threads = p.unit_walk_threads();
         m_binspr            = p.binspr();
         m_binspr            = false;     // prevent adventurous users from trying feature that isn't ready
         m_anf_simplify      = p.anf();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 2586fb537..c57aeeffe 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -117,8 +117,6 @@ namespace sat {
         bool               m_local_search;
         local_search_mode  m_local_search_mode;
         bool               m_local_search_dbg_flips;
-        unsigned           m_unit_walk_threads;
-        bool               m_unit_walk;
         bool               m_binspr;
         bool               m_cut_simplify;
         unsigned           m_cut_delay;
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index 191384582..78fd59a23 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -52,7 +52,6 @@ namespace sat {
         virtual ~extension() {}
         virtual void set_solver(solver* s) = 0;
         virtual void set_lookahead(lookahead* s) = 0;
-        virtual void set_unit_walk(unit_walk* u) = 0;
         virtual bool propagate(literal l, ext_constraint_idx idx) = 0;
         virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const = 0;
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index cdeac4536..36646006d 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -67,8 +67,6 @@ def_module_params('sat',
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),
                           ('local_search_dbg_flips', BOOL, False, 'write debug information for number of flips'),
-                          ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'),
-                          ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'),
                           ('binspr', BOOL, False, 'enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models'),
 	                  ('anf', BOOL, False, 'enable ANF based simplification in-processing'),
 	                  ('anf.delay', UINT, 2, 'delay ANF simplification by in-processing round'),
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index fa0258380..1572c610f 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -27,7 +27,6 @@ Revision History:
 #include "sat/sat_solver.h"
 #include "sat/sat_integrity_checker.h"
 #include "sat/sat_lookahead.h"
-#include "sat/sat_unit_walk.h"
 #include "sat/sat_ddfw.h"
 #include "sat/sat_prob.h"
 #include "sat/sat_anf_simplifier.h"
@@ -1194,7 +1193,7 @@ namespace sat {
             return do_local_search(num_lits, lits);
         }
         if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 || 
-             m_config.m_ddfw_threads > 0 || m_config.m_unit_walk_threads > 0) && !m_par) {
+             m_config.m_ddfw_threads > 0) && !m_par) {
             SASSERT(scope_lvl() == 0);
             return check_par(num_lits, lits);
         }
@@ -1214,10 +1213,6 @@ namespace sat {
             if (check_inconsistent()) return l_false;
             if (m_config.m_force_cleanup) do_cleanup(true);
 
-            if (m_config.m_unit_walk) {
-                return do_unit_walk();
-            }
-
             if (m_config.m_gc_burst) {
                 // force gc
                 m_conflicts_since_gc = m_gc_threshold + 1;
@@ -1326,19 +1321,6 @@ namespace sat {
         return invoke_local_search(num_lits, lits);
     }
 
-    lbool solver::do_unit_walk() {
-        unit_walk srch(*this);
-        lbool r = srch();
-        if (r == l_true) {
-            m_model.reset();
-            for (bool_var v = 0; v < num_vars(); ++v) {
-                m_model.push_back(m_assignment[literal(v,false).index()]);
-            }
-            m_model_is_current = true;
-        }
-        return r;
-    }
-
     lbool solver::check_par(unsigned num_lits, literal const* lits) {
         if (!rlimit().inc()) {
             return l_undef;
@@ -1347,9 +1329,8 @@ namespace sat {
         scoped_ptr_vector<solver> uw;
         int num_extra_solvers = m_config.m_num_threads - 1;
         int num_local_search  = static_cast<int>(m_config.m_local_search_threads);
-        int num_unit_walk = static_cast<int>(m_config.m_unit_walk_threads);
         int num_ddfw      = m_ext ? 0 : static_cast<int>(m_config.m_ddfw_threads);
-        int num_threads = num_extra_solvers + 1 + num_local_search + num_unit_walk + num_ddfw;        
+        int num_threads = num_extra_solvers + 1 + num_local_search + num_ddfw;        
         for (int i = 0; i < num_local_search; ++i) {
             local_search* l = alloc(local_search);
             l->updt_params(m_params);
@@ -1357,6 +1338,8 @@ namespace sat {
             l->set_seed(m_config.m_random_seed + i);
             ls.push_back(l);
         }
+
+        vector<reslimit> lims(num_ddfw);            
         // set up ddfw search
         for (int i = 0; i < num_ddfw; ++i) {
             ddfw* d = alloc(ddfw);
@@ -1365,23 +1348,11 @@ namespace sat {
             d->add(*this);
             ls.push_back(d);
         }
-
-        // set up unit walk
-        vector<reslimit> lims(num_unit_walk + num_ddfw);            
-        for (int i = 0; i < num_unit_walk; ++i) {
-            solver* s = alloc(solver, m_params,  lims[i]);
-            s->copy(*this);
-            s->m_config.m_unit_walk = true;
-            uw.push_back(s);
-        }
-
         int local_search_offset = num_extra_solvers;
-        int unit_walk_offset = num_extra_solvers + num_local_search + num_ddfw;
-        int main_solver_offset = unit_walk_offset + num_unit_walk;
+        int main_solver_offset = num_extra_solvers + num_local_search + num_ddfw;
 
 #define IS_AUX_SOLVER(i)   (0 <= i && i < num_extra_solvers)
-#define IS_LOCAL_SEARCH(i) (local_search_offset <= i && i < unit_walk_offset)
-#define IS_UNIT_WALK(i)    (unit_walk_offset <= i && i < main_solver_offset)
+#define IS_LOCAL_SEARCH(i) (local_search_offset <= i && i < main_solver_offset)
 #define IS_MAIN_SOLVER(i)  (i == main_solver_offset)
 
         sat::parallel par(*this);
@@ -1413,9 +1384,6 @@ namespace sat {
                 else if (IS_LOCAL_SEARCH(i)) {
                     r = ls[i-local_search_offset]->check(num_lits, lits, &par);
                 }
-                else if (IS_UNIT_WALK(i)) {
-                    r = uw[i-unit_walk_offset]->check(num_lits, lits);
-                }
                 else {
                     r = check(num_lits, lits);
                 }
@@ -1484,9 +1452,6 @@ namespace sat {
         if (result == l_true && IS_LOCAL_SEARCH(finished_id)) {
             set_model(ls[finished_id - local_search_offset]->get_model(), true);
         }
-        if (result == l_true && IS_UNIT_WALK(finished_id)) {
-            set_model(uw[finished_id - unit_walk_offset]->get_model(), true);
-        }
         if (!canceled) {
             rlimit().reset_cancel();
         }
diff --git a/src/sat/sat_unit_walk.cpp b/src/sat/sat_unit_walk.cpp
deleted file mode 100644
index 5e97adbdf..000000000
--- a/src/sat/sat_unit_walk.cpp
+++ /dev/null
@@ -1,514 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    sat_unit_walk.cpp
-
-Abstract:
-
-    unit walk local search procedure.
-
-    A variant of UnitWalk. Hirsch and Kojevinkov, SAT 2001.
-    This version uses a trail to reset assignments and integrates directly with the 
-    watch list structure. Thus, assignments are not delayed and we avoid treating
-    pending units as a multi-set. 
-
-    It uses standard DPLL approach for backracking, flipping the last decision literal that
-    lead to a conflict. It restarts after evern 100 conflicts.
-
-    It does not attempt to add conflict clauses 
-
-    It can receive conflict clauses from a concurrent CDCL solver 
-
-    The phase of variables is optionally sticky between rounds. We use a decay rate
-    to compute stickiness of a variable.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2017-12-15.
-
-Revision History:
-
-    2018-11-5:
-      change reinitialization to use local search with limited timeouts to find phase and ordering of variables.
-
---*/
-
-#include "sat/sat_unit_walk.h"
-#include "util/luby.h"
-
-
-namespace sat {
-
-    bool_var unit_walk::var_priority::peek(solver& s) {
-        while (m_head < m_vars.size()) {
-            bool_var v = m_vars[m_head];
-            unsigned idx = literal(v, false).index();
-            if (s.m_assignment[idx] == l_undef) {
-                // IF_VERBOSE(0, verbose_stream() << "pop " << v << "\n");
-                return v;            
-            }
-            ++m_head;
-        }
-        for (bool_var v : m_vars) {
-            if (s.m_assignment[literal(v, false).index()] == l_undef) {
-                IF_VERBOSE(0, verbose_stream() << "unassigned: " << v << "\n");
-            }
-        }
-        IF_VERBOSE(0, verbose_stream() << "#vars: " << m_vars.size() << "\n");
-        IF_VERBOSE(0, verbose_stream() << "(sat.unit-walk sat)\n");
-        return null_bool_var;
-    }
-
-    void unit_walk::var_priority::set_vars(solver& s) {
-        m_vars.reset();
-        s.pop_to_base_level();
-
-        for (unsigned v = 0; v < s.num_vars(); ++v) {            
-            if (!s.was_eliminated(v) && s.value(v) == l_undef) {
-                add(v);
-            }
-        }
-        IF_VERBOSE(0, verbose_stream() << "num vars " << m_vars.size() << "\n";);
-    }
-
-    bool_var unit_walk::var_priority::next(solver& s) {
-        bool_var v = peek(s);
-        ++m_head;
-        return v;
-    }
-
-    unit_walk::unit_walk(solver& s):
-        s(s) {
-        m_max_conflicts = 10000;
-        m_flips = 0;
-    }                        
-
-    class scoped_set_unit_walk {
-        solver& s;
-    public:
-        scoped_set_unit_walk(unit_walk* u, solver& s): s(s) {
-            if (s.get_extension()) s.get_extension()->set_unit_walk(u);
-        }
-        ~scoped_set_unit_walk() {
-            if (s.get_extension()) s.get_extension()->set_unit_walk(nullptr);
-        }
-    };
-
-    lbool unit_walk::operator()() {
-        m_inconsistent = false;
-        scoped_set_unit_walk _scoped_set(this, s);
-        if (init_runs())
-            return l_true;
-        init_propagation();
-        init_phase();
-        lbool st = l_undef;
-        while (s.rlimit().inc() && st == l_undef) {
-            if (inconsistent() && !m_decisions.empty()) do_pop();
-            else if (inconsistent()) st = l_false; 
-            else if (should_restart()) restart();
-            else if (should_backjump()) st = do_backjump();
-            else st = decide();
-        }
-        log_status();
-        return st;
-    }
-
-    void unit_walk::do_pop() {
-        update_max_trail();
-        ++s.m_stats.m_conflict;
-        pop();
-        propagate();
-    }
-
-    lbool unit_walk::decide() {
-        bool_var v = pqueue().next(s);
-        if (v == null_bool_var) {
-            return l_true;
-        }
-        literal lit(v, !m_phase[v]);
-        ++s.m_stats.m_decision;
-        m_decisions.push_back(lit);
-        pqueue().push();
-        assign(lit);
-        propagate();
-        return l_undef;
-    }
-
-    bool unit_walk::should_backjump() {
-        return 
-            s.m_stats.m_conflict >= m_max_conflicts && m_decisions.size() > 20;
-    } 
-
-    lbool unit_walk::do_backjump() {
-        unsigned backjump_level = m_decisions.size(); // - (m_decisions.size()/20);
-        lbool st = update_priority(backjump_level);
-        switch (st) {
-        case l_true: return l_true;
-        case l_false: break; // TBD
-        default: break;
-        }
-        if (refresh_solver())
-            return l_true;
-        return l_undef;
-    }
-
-    void unit_walk::pop() {
-        SASSERT (!m_decisions.empty());
-        literal dlit = m_decisions.back();
-        pop_decision();
-        assign(~dlit);
-    }
-
-    void unit_walk::pop_decision() {
-        SASSERT (!m_decisions.empty());
-        literal dlit = m_decisions.back();
-        literal lit;
-        do {
-            SASSERT(!m_trail.empty());
-            lit = m_trail.back(); 
-            s.m_assignment[lit.index()] = l_undef;
-            s.m_assignment[(~lit).index()] = l_undef;
-            m_trail.pop_back();
-        }
-        while (lit != dlit);
-        m_qhead = m_trail.size();
-        m_decisions.pop_back();
-        pqueue().pop();
-        m_inconsistent = false;
-    }
-
-    bool unit_walk::init_runs() {
-        m_luby_index = 0;
-        m_restart_threshold = 1000;
-        m_max_trail = 0;
-        m_trail.reset();
-        m_decisions.reset();
-        m_phase.resize(s.num_vars());
-        m_phase_tf.resize(s.num_vars(), ema(1e-5));
-        pqueue().reset();
-        pqueue().set_vars(s);
-        for (unsigned v = 0; v < s.num_vars(); ++v) {            
-            m_phase_tf[v].update(50);
-        }
-        m_ls.import(s, true);
-        m_rand.set_seed(s.rand()());
-        return l_true == update_priority(0);
-    }
-
-    lbool unit_walk::do_local_search(unsigned num_rounds) {
-        unsigned prefix_length = (0*m_trail.size())/10;
-        for (unsigned v = 0; v < s.num_vars(); ++v) {
-            m_ls.set_bias(v, m_phase_tf[v] >= 50 ? l_true : l_false);
-        }
-        for (literal lit : m_trail) {
-            m_ls.set_bias(lit.var(), lit.sign() ? l_false : l_true);
-        }
-        m_ls.rlimit().push(num_rounds);
-        lbool is_sat = m_ls.check(prefix_length, m_trail.c_ptr(), nullptr);
-        m_ls.rlimit().pop();
-        return is_sat;
-    }
-
-    lbool unit_walk::update_priority(unsigned level) {
-
-        while (m_decisions.size() > level) {
-            pop_decision();
-        }
-        IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk :update-priority " << m_decisions.size() << ")\n");
-
-        unsigned num_rounds = 50;
-        log_status();
-
-        lbool is_sat = do_local_search(num_rounds);
-        switch (is_sat) {
-        case l_true:
-            for (unsigned v = 0; v < s.num_vars(); ++v) {
-                s.m_assignment[v] = m_ls.get_model()[v];
-            } 
-            return l_true;
-        case l_false:
-            if (m_decisions.empty()) {
-                return l_false;
-            }
-            else {
-                pop();
-                return l_undef;
-            }
-        default:
-            update_pqueue();
-            return l_undef;
-        }        
-    }
-
-    /**
-     * \brief Reshuffle variables in the priority queue using the break counts from local search.
-     */
-    struct compare_break {
-        local_search& ls;
-        compare_break(local_search& ls): ls(ls) {}
-        int operator()(bool_var v, bool_var w) const {
-            return ls.get_priority(v) > ls.get_priority(w);
-        }
-    };
-
-    void unit_walk::update_pqueue() {
-        compare_break cb(m_ls);
-        std::sort(pqueue().begin(), pqueue().end(), cb);        
-        for (bool_var v : pqueue()) {
-            m_phase_tf[v].update(m_ls.cur_solution(v) ? 100 : 0);
-            m_phase[v] = l_true == m_ls.cur_solution(v);
-        }
-        pqueue().rewind();
-    }
-
-    void unit_walk::init_phase() {
-        for (bool_var v : pqueue()) {
-            m_phase[v] = s.m_phase[v];            
-        }
-    }
-
-    bool unit_walk::refresh_solver() {
-        m_max_conflicts += m_conflict_offset ;
-        m_conflict_offset += 10000;
-        if (s.m_par && s.m_par->copy_solver(s)) {
-            IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk fresh copy)\n";);
-            if (s.get_extension()) s.get_extension()->set_unit_walk(this);
-            if (init_runs())
-                return true;
-            init_phase();
-        }
-        return false;
-    }
-
-    bool unit_walk::should_restart() {
-        if (s.m_stats.m_conflict >= m_restart_threshold) {
-            m_restart_threshold = s.get_config().m_restart_initial * get_luby(m_luby_index);
-            ++m_luby_index;
-            return true;
-        }
-        return false;        
-    }
-
-    void unit_walk::restart() {
-        while (!m_decisions.empty()) {
-            pop_decision();
-        }
-    }
-
-    void unit_walk::update_max_trail() {
-        if (m_max_trail == 0 || m_trail.size() > m_max_trail) {
-            m_max_trail = m_trail.size();
-            m_restart_threshold += 10000;
-            m_max_conflicts = s.m_stats.m_conflict + 20000;
-            log_status();
-        }
-    }
-
-    void unit_walk::init_propagation() {
-        if (s.m_par && s.m_par->copy_solver(s)) {
-            IF_VERBOSE(1, verbose_stream() << "(sat.unit-walk fresh copy)\n";);
-            if (s.get_extension()) s.get_extension()->set_unit_walk(this);
-            init_runs();
-            init_phase();
-        }
-        for (literal lit : m_trail) {
-            s.m_assignment[lit.index()] = l_undef;
-            s.m_assignment[(~lit).index()] = l_undef;
-        }
-        m_flips = 0;
-        m_trail.reset();
-        s.m_stats.m_conflict = 0;
-        m_conflict_offset = 10000;
-        m_decisions.reset();
-        m_qhead = 0;
-        m_inconsistent = false;
-    }
-
-    void unit_walk::propagate() {
-        while (m_qhead < m_trail.size() && !inconsistent()) {
-            propagate(m_trail[m_qhead++]);         
-        }
-    }
-
-    std::ostream& unit_walk::display(std::ostream& out) const {
-        unsigned i = 0;
-        out << "num decisions: " << m_decisions.size() << "\n";
-        for (literal lit : m_trail) {
-            if (i < m_decisions.size() && m_decisions[i] == lit) {
-                out << "d " << i << ": ";
-                ++i;
-            }
-            out << lit << "\n";
-        }
-        s.display(verbose_stream());
-        return out;
-    }
-
-    void unit_walk::propagate(literal l) {
-        ++s.m_stats.m_propagate;
-        literal not_l = ~l;
-        literal l1, l2;
-        lbool val1, val2;
-        bool keep;
-        watch_list & wlist = s.get_wlist(l);
-        watch_list::iterator it  = wlist.begin();
-        watch_list::iterator it2 = it;
-        watch_list::iterator end = wlist.end();
-        for (; it != end; ++it) {
-            switch (it->get_kind()) {
-            case watched::BINARY:
-                l1 = it->get_literal();
-                switch (value(l1)) {
-                case l_false:
-                    conflict_cleanup(it, it2, wlist);
-                    set_conflict(l,l1);
-                    return;
-                case l_undef:
-                    assign(l1);
-                    break;
-                case l_true:
-                    break; // skip
-                }
-                *it2 = *it;
-                it2++;
-                break;
-            case watched::TERNARY:
-                l1 = it->get_literal1();
-                l2 = it->get_literal2();
-                val1 = value(l1);
-                val2 = value(l2);
-                if (val1 == l_false && val2 == l_undef) {
-                    assign(l2);
-                }
-                else if (val1 == l_undef && val2 == l_false) {
-                    assign(l1);
-                }
-                else if (val1 == l_false && val2 == l_false) {
-                    conflict_cleanup(it, it2, wlist);
-                    set_conflict(l,l1,l2);
-                    return;
-                }
-                *it2 = *it;
-                it2++;
-                break;
-            case watched::CLAUSE: {
-                if (value(it->get_blocked_literal()) == l_true) {
-                    *it2 = *it;
-                    it2++;
-                    break;
-                }
-                clause_offset cls_off = it->get_clause_offset();
-                clause & c = s.get_clause(cls_off);
-                if (c[0] == not_l)
-                    std::swap(c[0], c[1]);
-                if (c[1] != not_l) {
-                    *it2 = *it;
-                    it2++;
-                    break;
-                }
-                if (value(c[0]) == l_true) {
-                    it2->set_clause(c[0], cls_off);
-                    it2++;
-                    break;
-                }
-                SASSERT(c[1] == not_l);
-                literal * l_it  = c.begin() + 2;
-                literal * l_end = c.end();
-                for (; l_it != l_end; ++l_it) {
-                    if (value(*l_it) != l_false) {
-                        c[1]  = *l_it;
-                        *l_it = not_l;
-                        s.get_wlist((~c[1]).index()).push_back(watched(c[0], cls_off));
-                        goto end_clause_case;
-                    }
-                }
-                SASSERT(value(c[0]) == l_false || value(c[0]) == l_undef);
-                if (value(c[0]) == l_false) {
-                    c.mark_used();
-                    conflict_cleanup(it, it2, wlist);
-                    set_conflict(c);
-                    return;
-                }
-                else {
-                    *it2 = *it;
-                    it2++;
-                    assign(c[0]);
-                }
-                end_clause_case:
-                break;
-            }
-            case watched::EXT_CONSTRAINT:
-                SASSERT(s.get_extension());
-                keep = s.get_extension()->propagate(l, it->get_ext_constraint_idx());
-                if (inconsistent()) {
-                    if (!keep) {
-                        ++it;
-                    }
-                    set_conflict(l, l);
-                    conflict_cleanup(it, it2, wlist);
-                    return;
-                }
-                if (keep) {
-                    *it2 = *it;
-                    it2++;
-                }
-                break;
-            default:
-                UNREACHABLE();
-                break;
-            }
-        }
-        wlist.set_end(it2);
-    }
-
-    void unit_walk::assign(literal lit) {
-        VERIFY(value(lit) == l_undef);
-        s.m_assignment[lit.index()] = l_true;
-        s.m_assignment[(~lit).index()] = l_false;
-        m_trail.push_back(lit);
-        if (s.get_extension() && s.is_external(lit.var())) {
-            s.get_extension()->asserted(lit);       
-        } 
-        if (m_phase[lit.var()] == lit.sign()) {
-            ++m_flips;
-            flip_phase(lit);
-            m_phase_tf[lit.var()].update(m_phase[lit.var()] ? 100 : 0);        
-        }
-    }
-
-    void unit_walk::flip_phase(literal l) {
-        bool_var v = l.var();
-        m_phase[v] = !m_phase[v]; 
-    }
-
-    void unit_walk::log_status() {
-        IF_VERBOSE(1, verbose_stream() 
-                   << "(sat.unit-walk"
-                   << " :trail " << m_trail.size()
-                   << " :depth " << m_decisions.size()
-                   << " :decisions " << s.m_stats.m_decision
-                   << " :propagations " << s.m_stats.m_propagate
-                   << " :conflicts " << s.m_stats.m_conflict 
-                   << ")\n";);        
-    }
-
-    void unit_walk::set_conflict(literal l1, literal l2) {
-        set_conflict();
-    }
-
-    void unit_walk::set_conflict(literal l1, literal l2, literal l3) {
-        set_conflict();
-    }
-
-    void unit_walk::set_conflict(clause const& c) {
-        set_conflict();
-    }
-
-    void unit_walk::set_conflict() {
-        m_inconsistent = true; 
-    }
-    
-};
-
diff --git a/src/sat/sat_unit_walk.h b/src/sat/sat_unit_walk.h
deleted file mode 100644
index 620805873..000000000
--- a/src/sat/sat_unit_walk.h
+++ /dev/null
@@ -1,112 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    sat_unit_walk.h
-
-Abstract:
-
-    unit walk local search procedure.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2017-12-15.
-
-Revision History:
-
---*/
-#ifndef SAT_UNIT_WALK_H_
-#define SAT_UNIT_WALK_H_
-
-#include "sat/sat_solver.h"
-#include "sat/sat_local_search.h"
-#include "util/ema.h"
-
-namespace sat {
-
-    class unit_walk {
-#if 0
-        struct double2 {
-            double t, f;
-        };
-#endif
-        class var_priority {
-            svector<bool_var> m_vars;
-            unsigned_vector   m_lim;
-            unsigned          m_head;
-        public:
-            var_priority() { m_head = 0; }
-            void reset() { m_lim.reset(); m_head = 0;}
-            void rewind() { for (unsigned& l : m_lim) l = 0; m_head = 0;}
-            void add(bool_var v) { m_vars.push_back(v); }
-            bool_var next(solver& s);
-            bool_var peek(solver& s);
-            void set_vars(solver& s);
-            void push() { m_lim.push_back(m_head); }
-            void pop() { m_head = m_lim.back(); m_lim.pop_back(); }    
-            bool empty() const { return m_lim.empty(); }
-            bool_var const* begin() const { return m_vars.begin(); }
-            bool_var const* end() const { return m_vars.end(); }
-            bool_var* begin() { return m_vars.begin(); }
-            bool_var* end() { return m_vars.end(); }
-        };
-
-        solver&           s;
-        local_search      m_ls;
-        random_gen        m_rand;
-        bool_vector     m_phase;
-        svector<ema>      m_phase_tf;
-        var_priority      m_priorities;
-        unsigned          m_luby_index;
-        unsigned          m_restart_threshold;
-
-        // settings
-        unsigned          m_max_conflicts;
-
-        unsigned          m_flips;
-        unsigned          m_max_trail;
-        unsigned          m_qhead;
-        literal_vector    m_trail;
-        bool              m_inconsistent;
-        literal_vector    m_decisions;
-        unsigned          m_conflict_offset;
-        svector<lbool>    m_model;
-
-        bool should_restart();
-        void do_pop();
-        bool should_backjump();
-        lbool do_backjump();
-        lbool do_local_search(unsigned num_rounds);
-        lbool decide();
-        void restart();
-        void pop();
-        void pop_decision();
-        bool init_runs();
-        lbool update_priority(unsigned level);
-        void update_pqueue();
-        void init_phase();
-        void init_propagation();
-        bool refresh_solver();
-        void update_max_trail();
-        void flip_phase(literal l); 
-        void propagate();
-        void propagate(literal lit);
-        void set_conflict(literal l1, literal l2);
-        void set_conflict(literal l1, literal l2, literal l3);
-        void set_conflict(clause const& c);
-        inline lbool value(literal lit) { return s.value(lit); }
-        void log_status();
-        var_priority& pqueue() { return m_priorities; }
-    public:
-
-        unit_walk(solver& s);
-        lbool operator()();
-        std::ostream& display(std::ostream& out) const;
-        bool inconsistent() const { return m_inconsistent; }
-        void set_conflict();
-        void assign(literal lit);
-    };
-};
-
-#endif
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 59e0c81f6..f6afd539f 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -15,6 +15,8 @@ z3_add_component(smt
     seq_axioms.cpp
     seq_skolem.cpp
     seq_eq_solver.cpp
+    seq_ne_solver.cpp
+    seq_offset_eq.cpp
     smt_almost_cg_table.cpp
     smt_arith_value.cpp
     smt_case_split_queue.cpp
diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index 637e6b6ca..a6f8f6ab2 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -88,8 +88,12 @@ this translates to:
 
 void seq_axioms::add_extract_axiom(expr* e) {
     TRACE("seq", tout << mk_pp(e, m) << "\n";);
-    expr* s = nullptr, *i = nullptr, *l = nullptr;
-    VERIFY(seq.str.is_extract(e, s, i, l));
+    expr* _s = nullptr, *_i = nullptr, *_l = nullptr;
+    VERIFY(seq.str.is_extract(e, _s, _i, _l));
+    expr_ref s(_s, m), i(_i, m), l(_l, m);
+    m_rewrite(s);
+    m_rewrite(i);
+    if (l) m_rewrite(l);
     if (is_tail(s, i, l)) {
         add_tail_axiom(e, s);
         return;
@@ -294,14 +298,16 @@ void seq_axioms::tightest_prefix(expr* s, expr* x) {
    (len(s) <= len(t) -> i <= len(t)-len(s))
 */
 void seq_axioms::add_indexof_axiom(expr* i) {
-    expr* s = nullptr, *t = nullptr, *offset = nullptr;
+    expr* _s = nullptr, *_t = nullptr, *_offset = nullptr;
     rational r;
-    VERIFY(seq.str.is_index(i, t, s) ||
-           seq.str.is_index(i, t, s, offset));
+    VERIFY(seq.str.is_index(i, _t, _s) ||
+           seq.str.is_index(i, _t, _s, _offset));
     expr_ref minus_one(a.mk_int(-1), m);
     expr_ref zero(a.mk_int(0), m);
-    expr_ref xsy(m);
-    
+    expr_ref xsy(m), t(_t, m), s(_s, m), offset(_offset, m);
+    m_rewrite(t);
+    m_rewrite(s);
+    if (offset) m_rewrite(offset);
     literal cnt = mk_literal(seq.str.mk_contains(t, s));
     literal i_eq_m1 = mk_eq(i, minus_one);
     literal i_eq_0 = mk_eq(i, zero);
@@ -375,8 +381,11 @@ void seq_axioms::add_indexof_axiom(expr* i) {
 
  */
 void seq_axioms::add_last_indexof_axiom(expr* i) {
-    expr* s = nullptr, *t = nullptr;
-    VERIFY(seq.str.is_last_index(i, t, s));
+    expr* _s = nullptr, *_t = nullptr;
+    VERIFY(seq.str.is_last_index(i, _t, _s));
+    expr_ref s(_s, m), t(_t, m);
+    m_rewrite(s);
+    m_rewrite(t);
     expr_ref minus_one(a.mk_int(-1), m);
     expr_ref zero(a.mk_int(0), m);
     expr_ref s_head(m), s_tail(m);
@@ -417,8 +426,12 @@ void seq_axioms::add_last_indexof_axiom(expr* i) {
 
 */
 void seq_axioms::add_replace_axiom(expr* r) {
-    expr* u = nullptr, *s = nullptr, *t = nullptr;
-    VERIFY(seq.str.is_replace(r, u, s, t));
+    expr* _u = nullptr, *_s = nullptr, *_t = nullptr;
+    VERIFY(seq.str.is_replace(r, _u, _s, _t));
+    expr_ref u(_u, m), s(_s, m), t(_t, m);
+    m_rewrite(u);
+    m_rewrite(s);
+    m_rewrite(t);
     expr_ref x  = m_sk.mk_indexof_left(u, s);
     expr_ref y  = m_sk.mk_indexof_right(u, s);
     expr_ref xty = mk_concat(x, t, y);
@@ -445,8 +458,11 @@ void seq_axioms::add_replace_axiom(expr* r) {
 */
 void seq_axioms::add_at_axiom(expr* e) {
     TRACE("seq", tout << "at-axiom: " << ctx().get_scope_level() << " " << mk_bounded_pp(e, m) << "\n";);
-    expr* s = nullptr, *i = nullptr;
-    VERIFY(seq.str.is_at(e, s, i));
+    expr* _s = nullptr, *_i = nullptr;
+    VERIFY(seq.str.is_at(e, _s, _i));
+    expr_ref s(_s, m), i(_i, m);
+    m_rewrite(s);
+    m_rewrite(i);
     expr_ref zero(a.mk_int(0), m);
     expr_ref one(a.mk_int(1), m);
     expr_ref emp(seq.str.mk_empty(m.get_sort(e)), m);
@@ -465,7 +481,7 @@ void seq_axioms::add_at_axiom(expr* e) {
         }
         nth = es.back();
         es.push_back(m_sk.mk_tail(s, i));
-        add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, seq.str.mk_concat(es)));
+        add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, seq.str.mk_concat(es, m.get_sort(e))));
         add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(nth, e));                
     }
     else {
@@ -513,9 +529,11 @@ void seq_axioms::add_nth_axiom(expr* e) {
 
 
 void seq_axioms::add_itos_axiom(expr* e) {
-    expr* n = nullptr;
+    expr* _n = nullptr;
     TRACE("seq", tout << mk_pp(e, m) << "\n";);
-    VERIFY(seq.str.is_itos(e, n));
+    VERIFY(seq.str.is_itos(e, _n));
+    expr_ref n(_n, m);
+    m_rewrite(n);
 
     // itos(n) = "" <=> n < 0
     expr_ref zero(a.mk_int(0), m);
@@ -575,8 +593,10 @@ Define auxiliary function with the property:
  */
 void seq_axioms::add_stoi_axiom(expr* e, unsigned k) {
     SASSERT(k > 0);
-    expr* s = nullptr;
-    VERIFY (seq.str.is_stoi(e, s));    
+    expr* _s = nullptr;
+    VERIFY (seq.str.is_stoi(e, _s));
+    expr_ref s(_s, m);
+    m_rewrite(s);
     auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); }; 
     auto digit = [&](unsigned j) { return m_sk.mk_digit2int(mk_nth(s, j)); };
     expr_ref len = mk_len(s);
@@ -682,17 +702,20 @@ void seq_axioms::ensure_digit_axiom() {
    !(e1 < e2) or !(e2 < e1)
  */
 void seq_axioms::add_lt_axiom(expr* n) {
-    expr* e1 = nullptr, *e2 = nullptr;
-    VERIFY(seq.str.is_lt(n, e1, e2));
+    expr* _e1 = nullptr, *_e2 = nullptr;
+    VERIFY(seq.str.is_lt(n, _e1, _e2));
+    expr_ref e1(_e1, m), e2(_e2, m);
+    m_rewrite(e1);
+    m_rewrite(e2);
     sort* s = m.get_sort(e1);
     sort* char_sort = nullptr;
     VERIFY(seq.is_seq(s, char_sort));
     literal lt = mk_literal(n);
-    expr_ref x = m_sk.mk(symbol("str.lt.x"), e1, e2);
-    expr_ref y = m_sk.mk(symbol("str.lt.y"), e1, e2);
-    expr_ref z = m_sk.mk(symbol("str.lt.z"), e1, e2);
-    expr_ref c = m_sk.mk(symbol("str.lt.c"), e1, e2, char_sort);
-    expr_ref d = m_sk.mk(symbol("str.lt.d"), e1, e2, char_sort);
+    expr_ref x = m_sk.mk("str.<.x", e1, e2);
+    expr_ref y = m_sk.mk("str.<.y", e1, e2);
+    expr_ref z = m_sk.mk("str.<.z", e1, e2);
+    expr_ref c = m_sk.mk("str.<.c", e1, e2, char_sort);
+    expr_ref d = m_sk.mk("str.<.d", e1, e2, char_sort);
     expr_ref xcy = mk_concat(x, seq.str.mk_unit(c), y);
     expr_ref xdz = mk_concat(x, seq.str.mk_unit(d), z);
     literal eq   = mk_eq(e1, e2);
@@ -747,8 +770,11 @@ void seq_axioms::add_unit_axiom(expr* n) {
 */
 
 void seq_axioms::add_suffix_axiom(expr* e) {
-    expr* s = nullptr, *t = nullptr;
-    VERIFY(seq.str.is_suffix(e, s, t));
+    expr* _s = nullptr, *_t = nullptr;
+    VERIFY(seq.str.is_suffix(e, _s, _t));
+    expr_ref s(_s, m), t(_t, m);
+    m_rewrite(s);
+    m_rewrite(t);
     literal lit = mk_literal(e);
     literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
     sort* char_sort = nullptr;
@@ -764,8 +790,11 @@ void seq_axioms::add_suffix_axiom(expr* e) {
 }
 
 void seq_axioms::add_prefix_axiom(expr* e) {
-    expr* s = nullptr, *t = nullptr;
-    VERIFY(seq.str.is_prefix(e, s, t));
+    expr* _s = nullptr, *_t = nullptr;
+    VERIFY(seq.str.is_prefix(e, _s, _t));
+    expr_ref s(_s, m), t(_t, m);
+    m_rewrite(s);
+    m_rewrite(t);
     literal lit = mk_literal(e);
     literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
     sort* char_sort = nullptr;
@@ -806,6 +835,31 @@ void seq_axioms::add_length_axiom(expr* n) {
     }
 }
 
+/**
+   ~contains(a, b) => ~prefix(b, a)
+   ~contains(a, b) => ~contains(tail(a), b) or a = empty
+   ~contains(a, b) & a = empty => b != empty
+   ~(a = empty) => a = head + tail 
+ */
+void seq_axioms::unroll_not_contains(expr* e) {
+    expr_ref head(m), tail(m);
+    expr* a = nullptr, *b = nullptr;
+    VERIFY(seq.str.is_contains(e, a, b));
+    m_sk.decompose(a, head, tail);
+    expr_ref pref(seq.str.mk_prefix(b, a), m);
+    expr_ref postf(seq.str.mk_contains(tail, b), m);
+    m_rewrite(pref);
+    m_rewrite(postf);
+    literal pre = mk_literal(pref);
+    literal cnt = mk_literal(e);
+    literal ctail = mk_literal(postf);
+    literal emp = mk_eq_empty(a, true);
+    add_axiom(cnt, ~pre);
+    add_axiom(cnt, ~ctail);
+    add_axiom(~emp, mk_eq_empty(tail));
+    add_axiom(emp, mk_eq(a, seq.str.mk_concat(head, tail)));
+}
+
 
 expr_ref seq_axioms::add_length_limit(expr* s, unsigned k) {
     expr_ref bound_tracker  = m_sk.mk_length_limit(s, k);
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index 015f59791..1cf26edc3 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -86,6 +86,7 @@ namespace smt {
         void add_le_axiom(expr* n);
         void add_unit_axiom(expr* n);
         void add_length_axiom(expr* n);
+        void unroll_not_contains(expr* n);
 
         literal is_digit(expr* ch);
         literal mk_ge(expr* e, int k) { return mk_ge_e(e, a.mk_int(k)); }
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 78584d12d..4a21afd0a 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -31,15 +31,9 @@ bool theory_seq::solve_eqs(unsigned i) {
     context& ctx = get_context();
     bool change = false;
     for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
-        eq const& e = m_eqs[i];
-        if (solve_eq(e.ls(), e.rs(), e.dep(), i)) {
-            if (i + 1 != m_eqs.size()) {
-                eq e1 = m_eqs[m_eqs.size()-1];
-                m_eqs.set(i, e1);
-                --i;
-            }
+        if (solve_eq(i)) {
+            m_eqs.erase_and_swap(i--);
             ++m_stats.m_num_reductions;
-            m_eqs.pop_back();
             change = true;
         }
         TRACE("seq_verbose", display_equations(tout););
@@ -47,20 +41,23 @@ 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, unsigned idx) {
+bool theory_seq::solve_eq(unsigned idx) {
+    const eq& e = m_eqs[idx];
     context& ctx = get_context();
     expr_ref_vector& ls = m_ls;
     expr_ref_vector& rs = m_rs;
-    rs.reset(); ls.reset();
+    m_ls.reset();
+    m_rs.reset();
     dependency* dep2 = nullptr;
     bool change = false;
-    if (!canonize(l, ls, dep2, change)) return false;
-    if (!canonize(r, rs, dep2, change)) return false;
-    deps = m_dm.mk_join(dep2, deps);
-    TRACE("seq_verbose", tout << l << " = " << r << " ==> ";
+    if (!canonize(e.ls(), ls, dep2, change)) return false;
+    if (!canonize(e.rs(), rs, dep2, change)) return false;
+    dependency* deps = m_dm.mk_join(dep2, e.dep());
+    TRACE("seq_verbose", 
+          tout << e.ls() << " = " << e.rs() << " ==> ";
           tout << ls << " = " << rs << "\n";
-          display_deps(tout, deps);
-          );
+          display_deps(tout, deps););
+
     if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
         TRACE("seq", tout << "simplified\n";);
         return true;
@@ -91,22 +88,16 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
     }
     if (!ctx.inconsistent() && change) {
         // The propagation step from arithmetic state (e.g. length offset) to length constraints
-        if (get_context().get_scope_level() == 0) {
-            prop_arith_to_len_offset();
-        }
         TRACE("seq", tout << "inserting equality\n";);
-        bool updated = false;
         expr_ref_vector new_ls(m);
-        if (!m_len_offset.empty() && 
-            find_better_rep(ls, rs, idx, deps, new_ls)) {
+        if (!m_offset_eq.empty() && find_better_rep(ls, rs, idx, deps, new_ls)) {
             // Find a better equivalent term for lhs of an equation based on length constraints            
             m_eqs.push_back(eq(m_eq_id++, new_ls, rs, deps));
+            return true;
         }
         else {
-            m_eqs.push_back(eq(m_eq_id++, ls, rs, deps));
+            m_eqs.set(idx, eq(m_eq_id++, ls, rs, deps)); 
         }
-        TRACE("seq", tout << "simplified\n";);
-        return true;
     }
     return false;
 }
@@ -138,10 +129,8 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
     context& ctx = get_context();
     ptr_vector<expr> xs, ys;
     expr_ref x(m), y(m);
-    bool is_binary = 
-        is_binary_eq(ls, rs, x, xs, ys, y) || 
-        is_binary_eq(rs, ls, x, xs, ys, y);
-    if (!is_binary) {
+    if (!is_binary_eq(ls, rs, x, xs, ys, y) &&
+        !is_binary_eq(rs, ls, x, xs, ys, y)) {
         return false;
     }
     // Equation is of the form x ++ xs = ys ++ y
@@ -227,9 +216,44 @@ bool theory_seq::occurs(expr* a, expr* b) {
     return false;
 }
 
-// TODO: propagate length offsets for last vars
+/**
+   \brief
+
+   This step performs destructive superposition
+
+   Based on the implementation it would do the following:
+  
+   e:   l1 + l2 + l3 + l = r1 + r2 + r
+   G |- len(l1) = len(l2) = len(r1) = 0
+   e':  l1 + l2 + l3 + l = r3 + r'         occurs prior to e among equations
+   G |- len(r3) = len(r2)
+   r2, r3 are not identical
+   ----------------------------------
+   e'' : l1 + l2 + l3 + l = r3 + r'
+
+   e:   l1 + l2 + l3 + l = r1 + r2 + r
+   G |- len(l1) = len(l2) = len(r1) = 0
+   e':  l1 + l2 + l3 + l = r3 + r'         occurs prior to e among equations
+   G |- len(r3) = len(r2) + offset
+   r2, r3 are not identical
+   ----------------------------------
+   e'' : l1 + l2 + l3 + l = r3 + r'       
+
+   NB, this doesn't make sense because e'' is just e', which already occurs.
+   It doesn't inherit the constraints from e either, which would get lost.
+
+   NB, if len(r3) = len(r2) would be used, then the justification for the equality
+   needs to be tracked in dependencies.
+    
+   TODO: propagate length offsets for last vars
+
+*/
 bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned idx,
                                  dependency*& deps, expr_ref_vector & res) {
+
+    // disabled until functionality is clarified
+    return false;
+
     context& ctx = get_context();
 
     if (ls.empty() || rs.empty())
@@ -251,7 +275,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
 
     // Offset = 0, No change
     if (l_fst && get_root(len_l_fst) == root2) {
-        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
+        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst, m) << ")\n";);
         return false;
     }
 
@@ -265,7 +289,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
             nl_fst = e.rs().get(0);
         if (nl_fst && nl_fst != r_fst && root2 == get_root(mk_len(nl_fst))) {
             res.reset();
-            res.append(e.rs().size(), e.rs().c_ptr());
+            res.append(e.rs());
             deps = m_dm.mk_join(e.dep(), deps);
             return true;
         }
@@ -273,38 +297,27 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
     // Offset != 0, No change
     if (l_fst && ctx.e_internalized(len_l_fst)) {
         enode * root1 = get_root(len_l_fst);
-        obj_map<enode, int> tmp;
-        int offset;
-        if (!m_autil.is_numeral(root1->get_owner()) && !m_autil.is_numeral(root2->get_owner())) {
-            if (m_len_offset.find(root1, tmp) && tmp.find(root2, offset)) {
-                TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
-                find_max_eq_len(ls, rs);
-                return false;
-            }
-            else if (m_len_offset.find(root2, tmp) && tmp.find(root1, offset)) {
-                TRACE("seq", tout << "(" << mk_pp(r_fst, m) << ", " << mk_pp(l_fst,m) << ")\n";);
-                find_max_eq_len(ls ,rs);
-                return false;
-            }
+        if (m_offset_eq.contains(root1, root2)) {
+            TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_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)) {
+    if (m_offset_eq.contains(root2)) {
         for (unsigned i = 0; i < idx; ++i) {
             eq const& e = m_eqs[i];
             if (e.ls() != ls) continue;
             expr* nl_fst = nullptr;
-            if (e.rs().size()>1 && is_var(e.rs().get(0)))
+            if (e.rs().size() > 1 && is_var(e.rs().get(0)))
                 nl_fst = e.rs().get(0);
             if (nl_fst && nl_fst != r_fst) {
-                int offset;
                 expr_ref len_nl_fst = mk_len(nl_fst);
                 if (ctx.e_internalized(len_nl_fst)) {
-                    enode * root1 = ctx.get_enode(len_nl_fst)->get_root();
-                    if (!m_autil.is_numeral(root1->get_owner()) && tmp.find(root1, offset)) {
+                    enode * root1 = get_root(len_nl_fst);
+                    if (m_offset_eq.contains(root2, root1)) {
                         res.reset();
-                        res.append(e.rs().size(), e.rs().c_ptr());
+                        res.append(e.rs());
                         deps = m_dm.mk_join(e.dep(), deps);
                         find_max_eq_len(res, rs);
                         return true;
@@ -329,12 +342,12 @@ bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const
     expr_ref len_l_fst = mk_len(l_fst);
     if (!ctx.e_internalized(len_l_fst)) 
         return false;
-    enode * root1 = ctx.get_enode(len_l_fst)->get_root();
+    enode * root1 = get_root(len_l_fst);
 
     expr_ref len_r_fst = mk_len(r_fst);
     if (!ctx.e_internalized(len_r_fst))
         return false;
-    enode* root2 = ctx.get_enode(len_r_fst)->get_root();
+    enode* root2 = get_root(len_r_fst);
 
     if (root1 == root2) {
         TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
@@ -342,43 +355,30 @@ bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const
         return true;
     }
 
-    if (m_autil.is_numeral(root1->get_owner()) || m_autil.is_numeral(root2->get_owner())) 
-        return false;
-
-    obj_map<enode, int> tmp;
-    if (m_len_offset.find(root1, tmp) && tmp.find(root2, offset)) {
-        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
-        return true;
-    }
-    if (m_len_offset.find(root2, tmp) && tmp.find(root1, offset)) {
-        offset = -offset;
-        TRACE("seq", tout << "(" << mk_pp(r_fst, m) << ", " << mk_pp(l_fst,m) << ")\n";);
+    if (m_offset_eq.find(root1, root2, offset)) {
+        TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << " " << offset << ")\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]););
-                }
+    if (false && m_offset_eq.propagate() && !m_offset_eq.empty()) {
+        // NB: disabled until find_better_rep is handled.
+#if 0
+        for (unsigned i = m_eqs.size(); i-- > 0; ) {
+            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());
+                m_eqs.set(i, eq(m_eq_id++, new_ls, rs, deps));
+                TRACE("seq", display_equation(tout, m_eqs[i]););
             }
         }
+#endif
     }
 
     for (auto const& e : m_eqs) {
@@ -389,44 +389,60 @@ bool theory_seq::len_based_split() {
     return false;
 }
 
+/*
+   
+   ls = x11 + x12                for len(x11) = len(y11)
+   rs = y11 + y12
+
+   ls = x11     + Z + x12        for len(x11) = len(y11) + offset
+   rs = y11 + Z + y12
+
+   ls = x11 + Z + x12            for len(x11) = len(y11) - offset
+   rs = y11     + Z + y12
+
+   Use last case as sample:
+
+   propagate ls = rs & len(x12 + Z) == len(y11) => x11 + Z == y11
+   propagate ls = rs & len(x11 + Z) == len(y11) => x12 == Z + y12
+   propagate ls = rs & len(x12 + Z) == len(y11) => len(Z) = offset
+   propagate ls = rs & len(ls[2:]) == len(rs[2:]) => ls[2:] == rs[2:]
+   
+*/
+
 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))
+    int offset = 0;
+    if (!has_len_offset(ls, rs, offset))
         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);
+    sort* srt = m.get_sort(ls[0]);
+    expr_ref x11 = expr_ref(ls[0], m);
+    expr_ref x12 = mk_concat(ls.size()-1, ls.c_ptr()+1, srt);
+    expr_ref y11 = expr_ref(rs[0], m);
+    expr_ref y12 = mk_concat(rs.size()-1, rs.c_ptr()+1, srt);
 
     expr_ref lenX11 = mk_len(x11);
-    expr_ref lenY11(m);
+    expr_ref lenY11 = mk_len(y11);
     expr_ref Z(m);
-    int offset = 0;
-    if (offset_orig != 0) {
-        lenY11 = m_autil.mk_add(mk_len(y11), m_autil.mk_int(offset_orig));
-        if (offset_orig > 0) {
-            offset = offset_orig;
+    if (offset != 0) {
+        lenY11 = m_autil.mk_add(lenY11, m_autil.mk_int(offset));
+        if (offset > 0) {
             Z = m_sk.mk_align(y12, x12, x11, y11);
             y11 = mk_concat(y11, Z);
             x12 = mk_concat(Z, x12);
         }
         else {
-            offset = -offset_orig;
+            offset = -offset;
             Z = m_sk.mk_align(x12, y12, y11, x11);
             x11 = mk_concat(x11, Z);
             y12 = mk_concat(Z, y12);
         }
     }
-    else {
-        lenY11 = mk_len(y11);
-    }
 
     dependency* dep = e.dep();
     literal_vector lits;
@@ -444,27 +460,13 @@ bool theory_seq::len_based_split(eq const& e) {
         for (unsigned i = 2; i < rs.size(); ++i) {
             len2 = mk_add(len2, mk_len(rs[i]));
         }
-        literal lit2;
-        if (!m_autil.is_numeral(len1) && !m_autil.is_numeral(len2)) {
-            lit2 = mk_eq(len1, len2, false);           
-        }
-        else {
-            expr_ref eq_len(m.mk_eq(len1, len2), m);
-            lit2 = mk_literal(eq_len);            
-        }
+        literal lit2 = mk_eq(len1, len2, false);
         
         if (ctx.get_assignment(lit2) == l_true) {           
             lits.push_back(lit2);
-            TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";);
-            expr_ref lhs(m), rhs(m);
-            if (ls.size() > 2)
-                lhs = m_util.str.mk_concat(ls.size()-2, ls.c_ptr()+2);
-            else
-                lhs = m_util.str.mk_empty(m.get_sort(x11));
-            if (rs.size() > 2)
-                rhs = m_util.str.mk_concat(rs.size()-2, rs.c_ptr()+2);
-            else
-                rhs = m_util.str.mk_empty(m.get_sort(x11));
+            TRACE("seq", tout << len1 << " = " << len2 << "\n";);
+            expr_ref lhs = mk_concat(ls.size()-2, ls.c_ptr()+2, srt);
+            expr_ref rhs = mk_concat(rs.size()-2, rs.c_ptr()+2, srt);
             propagate_eq(dep, lits, lhs, rhs, true);
             lits.pop_back();
         }
@@ -622,7 +624,7 @@ bool theory_seq::split_lengths(dependency* dep,
     else if (m_util.str.is_unit(Y)) {
         SASSERT(lenB == lenX);
         bs.push_back(Y);
-        expr_ref bY(m_util.str.mk_concat(bs), m);
+        expr_ref bY = mk_concat(bs, m.get_sort(Y));
         propagate_eq(dep, lits, X, bY, true);
     }
     else {
@@ -655,13 +657,9 @@ bool theory_seq::branch_binary_variable(eq const& e) {
     }
     ptr_vector<expr> xs, ys;
     expr_ref x(m), y(m);
-    bool is_binary = is_binary_eq(e.ls(), e.rs(), x, xs, ys, y);
-    if (!is_binary) {
-        is_binary = is_binary_eq(e.rs(), e.ls(), x, xs, ys, y);
-    }
-    if (!is_binary) {
+    if (!is_binary_eq(e.ls(), e.rs(), x, xs, ys, y) &&
+        !is_binary_eq(e.rs(), e.ls(), x, xs, ys, y))
         return false;
-    }
     if (x == y) {
         return false;
     }
@@ -760,7 +758,7 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
     else {
         literal lit = mk_eq(m_autil.mk_int(lX), mk_len(X), false);
         if (l_true == ctx.get_assignment(lit)) {
-            expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m);
+            expr_ref R = mk_concat(lX, units.c_ptr(), m.get_sort(X));
             propagate_eq(dep, lit, X, R);
             TRACE("seq", tout << "propagate " << mk_pp(X, m) << " " << R << "\n";);
         }
@@ -794,7 +792,7 @@ bool theory_seq::branch_ternary_variable2() {
     return false;
 }
 
-bool theory_seq::eq_unit(expr* const& l, expr* const &r) const {
+bool theory_seq::eq_unit(expr* l, expr* r) const {
     return l == r || is_unit_nth(l) || is_unit_nth(r);
 }
 
@@ -866,49 +864,42 @@ unsigned_vector theory_seq::overlap2(expr_ref_vector const& ls, expr_ref_vector
 
 bool theory_seq::branch_ternary_variable_base(
     dependency* dep, unsigned_vector const& indexes,
-    expr* const& x, expr_ref_vector const& xs, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
+    expr* x, expr_ref_vector const& xs, expr* y1, expr_ref_vector const& ys, expr* 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));
-        }
+        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)));
-        if (ctx.get_assignment(lit1) == l_undef) {
+        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;
-            continue;
-        }
-        else if (ctx.get_assignment(lit1) == l_true) {
+            break;
+        case l_true: 
             TRACE("seq", tout << "base case: true branch\n";);
-            literal_vector lits;
-            lits.push_back(lit1);
-            propagate_eq(dep, lits, y2, xs2E, true);
+            propagate_eq(dep, lit1, y2, xs2E, true);
             if (ind > ys.size()) {
-                expr_ref xs1E(m_util.str.mk_concat(ind-ys.size(), xs.c_ptr()), m);
+                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, lits, xxs1E, y1, true);
+                propagate_eq(dep, lit1, xxs1E, y1, true);
             }
             else if (ind == ys.size()) {
-                propagate_eq(dep, lits, x, y1, true);
+                propagate_eq(dep, lit1, x, y1, true);
             }
             else {
-                expr_ref ys1E(m_util.str.mk_concat(ys.size()-ind, ys.c_ptr()), m);
+                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, lits, x, y1ys1E, true);
+                propagate_eq(dep, lit1, x, y1ys1E, true);
             }
             return true;
-        }
-        else {
+        default:
             TRACE("seq", tout << "base case: false branch\n";);
-            continue;
+            break;
         }
     }
     return change;
@@ -918,11 +909,8 @@ bool theory_seq::branch_ternary_variable_base(
 bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x(m), y1(m), y2(m);
-    bool is_ternary = is_ternary_eq(e.ls(), e.rs(), x, xs, y1, ys, y2, flag1);
-    if (!is_ternary) {
-        is_ternary = is_ternary_eq(e.rs(), e.ls(), x, xs, y1, ys, y2, flag1);
-    }
-    if (!is_ternary) {
+    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)) {
         return false;
     }
 
@@ -985,49 +973,42 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
     return true;
 }
 
-bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector const& indexes,
-        expr_ref_vector const& xs, expr* const& x, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
+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) {
     context& ctx = get_context();
+    sort* srt = m.get_sort(x);
     bool change = false;
     for (auto ind : indexes) {
-        expr_ref xs1E(m);
-        if (ind > 0) {
-            xs1E = m_util.str.mk_concat(ind, xs.c_ptr());
-        }
-        else {
-            xs1E = m_util.str.mk_empty(m.get_sort(x));
-        }
-        literal lit1 = mk_literal(m_autil.mk_le(mk_len(y1), m_autil.mk_int(ind)));
-        if (ctx.get_assignment(lit1) == l_undef) {
+        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(lit1);
-            ctx.force_phase(lit1);
+            ctx.mark_as_relevant(le);
+            ctx.force_phase(le);
             change = true;
-            continue;
-        }
-        else if (ctx.get_assignment(lit1) == l_true) {
+            break;
+        case l_true: 
             TRACE("seq", tout << "base case: true branch\n";);
-            literal_vector lits;
-            lits.push_back(lit1);
-            propagate_eq(dep, lits, y1, xs1E, true);
+            propagate_eq(dep, le, 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 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, lits, xs2x, y2, true);
+                propagate_eq(dep, le, xs2x, y2, true);
             }
             else if (xs.size() - ind == ys.size()) {
-                propagate_eq(dep, lits, x, y2, true);
+                propagate_eq(dep, le, 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 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, lits, x, ys1y2, true);
+                propagate_eq(dep, le, x, ys1y2, true);
             }
             return true;
-        }
-        else {
+        default:
             TRACE("seq", tout << "base case: false branch\n";);
-            continue;
+            break;
         }
     }
     return change;
@@ -1037,13 +1018,9 @@ bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector
 bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x(m), y1(m), y2(m);
-    bool is_ternary = is_ternary_eq2(e.ls(), e.rs(), xs, x, y1, ys, y2, flag1);
-    if (!is_ternary) {
-        is_ternary = is_ternary_eq2(e.rs(), e.ls(), xs, x, y1, ys, y2, flag1);
-    }
-    if (!is_ternary) {
+    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))
         return false;
-    }
 
     rational lenX, lenY1, lenY2;
     context& ctx = get_context();
@@ -1078,21 +1055,18 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
     }
     else {
         literal ge = m_ax.mk_ge(mk_len(y1), xs.size());
-        if (ctx.get_assignment(ge) == l_undef) {
+        switch (ctx.get_assignment(ge)) {
+        case l_undef:
             TRACE("seq", tout << "rec case init\n";);
             ctx.mark_as_relevant(ge);
             ctx.force_phase(ge);
-        }
-        else if (ctx.get_assignment(ge) == l_true) {
-            TRACE("seq", tout << "true branch\n";);
-            TRACE("seq", display_equation(tout, e););
-            literal_vector lits;
-            lits.push_back(ge);
-            dependency* dep = e.dep();
-            propagate_eq(dep, lits, x, Zysy2, true);
-            propagate_eq(dep, lits, y1, xsZ, true);
-        }
-        else {
+            break;
+        case l_true:
+            TRACE("seq", display_equation(tout << "true branch\n", e););
+            propagate_eq(e.dep(), ge, x,  Zysy2, true);
+            propagate_eq(e.dep(), ge, y1, xsZ, true);
+            break;
+        default:
             return branch_ternary_variable_base2(e.dep(), indexes, xs, x, y1, ys, y2);
         }
     }
@@ -1112,19 +1086,17 @@ bool theory_seq::branch_quat_variable() {
 // Equation is of the form x1 ++ xs ++ x2 = y1 ++ ys ++ y2 where xs, ys are units.
 bool theory_seq::branch_quat_variable(eq const& e) {
     expr_ref_vector xs(m), ys(m);
-    expr_ref x1_l(m), x2(m), y1_l(m), y2(m);
-    bool is_quat = is_quat_eq(e.ls(), e.rs(), x1_l, xs, x2, y1_l, ys, y2);
-    if (!is_quat) {
+    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;
-    }
     
     rational lenX1, lenX2, lenY1, lenY2;
     context& ctx = get_context();
-    if (!get_length(x1_l, lenX1)) {
-        add_length_to_eqc(x1_l);
+    if (!get_length(x1, lenX1)) {
+        add_length_to_eqc(x1);
     }
-    if (!get_length(y1_l, lenY1)) {
-        add_length_to_eqc(y1_l);
+    if (!get_length(y1, lenY1)) {
+        add_length_to_eqc(y1);
     }
     if (!get_length(x2, lenX2)) {
         add_length_to_eqc(x2);
@@ -1138,101 +1110,44 @@ bool theory_seq::branch_quat_variable(eq const& e) {
     expr_ref xsx2 = mk_concat(xs);
     ys.push_back(y2);
     expr_ref ysy2 = mk_concat(ys);
-    expr_ref x1(x1_l, m);
-    expr_ref y1(y1_l, m);
-    expr_ref sub(mk_sub(mk_len(x1_l), mk_len(y1_l)), m);
+    expr_ref sub(mk_sub(mk_len(x1), mk_len(y1)), m);
     literal le = m_ax.mk_le(sub, 0);
-    literal_vector lits;
-    if (ctx.get_assignment(le) == l_undef) {
+
+    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);
-    }
-    else if (ctx.get_assignment(le) == l_false) {
+        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);
-        lits.push_back(~le);
         dependency* dep = e.dep();
-        propagate_eq(dep, lits, x1, y1Z1, true);
-        propagate_eq(dep, lits, Z1xsx2, ysy2, true);
+        propagate_eq(dep, ~le, x1, y1Z1, true);
+        propagate_eq(dep, ~le, Z1xsx2, ysy2, true);
+        break;
     }
-    else if (ctx.get_assignment(le) == l_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);
-        lits.push_back(le);
         dependency* dep = e.dep();
-        propagate_eq(dep, lits, x1Z2, y1, true);
-        propagate_eq(dep, lits, xsx2, Z2ysy2, true);
+        propagate_eq(dep, le, x1Z2, y1, true);
+        propagate_eq(dep, le, xsx2, Z2ysy2, true);
+        break;
+    }
     }
     return true;
 }
 
-void theory_seq::len_offset(expr* e, rational val) {
-    context & ctx = get_context();
-    expr *l1 = nullptr, *l2 = nullptr, *l21 = nullptr, *l22 = nullptr;
-    rational fact;
-    if (m_autil.is_add(e, l1, l2) && m_autil.is_mul(l2, l21, l22) &&
-        m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
-        if (ctx.e_internalized(l1) && ctx.e_internalized(l22)) {
-            enode* r1 = get_root(l1), *n1 = r1;
-            enode* r2 = get_root(l22), *n2 = r2;
-            expr *e1 = nullptr, *e2 = nullptr;
-            do {
-                if (m_util.str.is_length(n1->get_owner(), e1))
-                    break;
-                n1 = n1->get_next();               
-            }
-            while (n1 != r1);
-            do {
-                if (m_util.str.is_length(n2->get_owner(), e2)) 
-                    break;
-                n2 = n2->get_next();                
-            }
-            while (n2 != r2);
-            obj_map<enode, int> tmp;
-            if (m_util.str.is_length(n1->get_owner(), e1)
-                && m_util.str.is_length(n2->get_owner(), e2) &&                
-                m_len_offset.find(r1, tmp)) {
-                tmp.insert(r2, val.get_int32());
-                m_len_offset.insert(r1, tmp);
-                TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";);
-                return;
-            }
-        }
-    }
-}
-
-// Find the length offset from the congruence closure core
-void theory_seq::prop_arith_to_len_offset() {
-    context & ctx = get_context();
-    obj_hashtable<enode> const_set;
-    ptr_vector<enode>::const_iterator it  = ctx.begin_enodes();
-    ptr_vector<enode>::const_iterator end = ctx.end_enodes();
-    for (; it != end; ++it) {
-        enode * root = (*it)->get_root();
-        rational val;
-        if (m_autil.is_numeral(root->get_owner(), val) && val.is_neg()) {
-            if (const_set.contains(root)) continue;
-            const_set.insert(root);
-            TRACE("seq", tout << "offset: " << mk_pp(root->get_owner(), m) << "\n";);
-            enode *next = root->get_next();
-            while (next != root) {
-                TRACE("seq", tout << "eqc: " << mk_pp(next->get_owner(), m) << "\n";);
-                len_offset(next->get_owner(), val);
-                next = next->get_next();
-            }
-        }
-    }
-}
 
 int theory_seq::find_fst_non_empty_idx(expr_ref_vector const& xs) {
     context & ctx = get_context();    
@@ -1415,26 +1330,7 @@ unsigned theory_seq::find_branch_start(unsigned k) {
     return 0;
 }
 
-expr_ref_vector theory_seq::expand_strings(expr_ref_vector const& es) {
-    expr_ref_vector ls(m);
-    for (expr* e : es) {
-        zstring s;
-        if (m_util.str.is_string(e, s)) {
-            for (unsigned i = 0; i < s.length(); ++i) {
-                ls.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, i)));
-            }
-        }
-        else {
-            ls.push_back(e);
-        }
-    }
-    return ls;
-}
-
-bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& _ls, expr_ref_vector const& _rs) {
-    expr_ref_vector ls = expand_strings(_ls);
-    expr_ref_vector rs = expand_strings(_rs);
-
+bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs) {
     if (ls.empty()) {
         return false;
     }
@@ -1474,10 +1370,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
 
     bool all_units = true;
     for (expr* r : rs) {
-        if (!m_util.str.is_unit(r)) {
-            all_units = false;
-            break;
-        }
+        all_units &= m_util.str.is_unit(r);
     }
     if (all_units) {
         context& ctx = get_context();
@@ -1593,7 +1486,7 @@ bool theory_seq::propagate_length_coherence(expr* e) {
     expr_ref_vector elems(m);
     unsigned _lo = lo.get_unsigned();
     for (unsigned j = 0; j < _lo; ++j) {
-        mk_decompose(seq, head, tail);
+        m_sk.decompose(seq, head, tail);
         elems.push_back(head);
         seq = tail;
     }
@@ -1630,7 +1523,7 @@ bool theory_seq::check_length_coherence(expr* e) {
             expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
             expr_ref head(m), tail(m);
             // e = emp \/ e = unit(head.elem(e))*tail(e)
-            mk_decompose(e, head, tail);
+            m_sk.decompose(e, head, tail);
             expr_ref conc = mk_concat(head, tail);
             if (propagate_is_conc(e, conc)) {
                 assume_equality(tail, emp);
@@ -1756,6 +1649,7 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
     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;
+        sort* srt = m.get_sort(ls[0]);
         for (; l_start < ls.size()-1; ++l_start) {
             if (m_util.str.is_unit(ls[l_start])) break;
         }
@@ -1783,12 +1677,12 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
         }
         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);
+        x1 = mk_concat(l_start, ls.c_ptr(), srt);
+        x2 = mk_concat(ls.size()-l_end-1, ls.c_ptr()+l_end+1, srt);
         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);
+        y1 = mk_concat(r_start, rs.c_ptr(), srt);
+        y2 = mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1, srt);
         return true;
     }
     return false;
@@ -1802,6 +1696,7 @@ bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const&
                                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())) {
+        sort* srt = m.get_sort(ls[0]);
         unsigned l_start = ls.size()-1;
         for (; l_start > 0; --l_start) {
             if (!m_util.str.is_unit(ls[l_start])) break;
@@ -1826,11 +1721,11 @@ bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const&
         }
         xs.reset();
         xs.append(ls.size()-l_start, ls.c_ptr()+l_start);
-        x = m_util.str.mk_concat(l_start, ls.c_ptr());
+        x = mk_concat(l_start, ls.c_ptr(), srt);
         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);
+        y1 = mk_concat(r_start, rs.c_ptr(), srt);
+        y2 = mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1, srt);
         return true;
     }
     return false;
@@ -1844,6 +1739,7 @@ bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const
                                 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())) {
+        sort* srt = m.get_sort(ls[0]);
         unsigned l_start = 0;
         for (; l_start < ls.size()-1; ++l_start) {
             if (!m_util.str.is_unit(ls[l_start])) break;
@@ -1867,11 +1763,11 @@ bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const
         }
         xs.reset();
         xs.append(l_start, ls.c_ptr());
-        x = m_util.str.mk_concat(ls.size()-l_start, ls.c_ptr()+l_start);
+        x = mk_concat(ls.size()-l_start, ls.c_ptr()+l_start, srt);
         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);
+        y1 = mk_concat(r_start, rs.c_ptr(), srt);
+        y2 = mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1, srt);
         return true;
     }
     return false;
@@ -1890,7 +1786,7 @@ bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const&
         expr_ref_vector ls1(m), rs1(m); 
         expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m);
         m_rewrite(idx1);
-        expr_ref rhs(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m);
+        expr_ref rhs = mk_concat(rs.size(), rs.c_ptr(), m.get_sort(ls[0]));
         ls1.push_back(s);        
         if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx)); 
         rs1.push_back(m_util.str.mk_unit(rhs)); 
diff --git a/src/smt/seq_ne_solver.cpp b/src/smt/seq_ne_solver.cpp
new file mode 100644
index 000000000..3ddbfcfa8
--- /dev/null
+++ b/src/smt/seq_ne_solver.cpp
@@ -0,0 +1,303 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    seq_ne_solver.cpp
+
+Abstract:
+
+    Features from theory_seq that are specific to solving dis-equations.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-6-12
+*/
+
+#include <typeinfo>
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/ast_trail.h"
+#include "ast/for_each_expr.h"
+#include "smt/smt_context.h"
+#include "smt/theory_seq.h"
+#include "smt/theory_arith.h"
+
+using namespace smt;
+
+bool theory_seq::solve_nqs(unsigned i) {
+    context & ctx = get_context();
+    for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
+        if (solve_ne(i)) {
+            if (i + 1 != m_nqs.size()) {
+                ne n = m_nqs[m_nqs.size()-1];
+                m_nqs.set(i, n);
+                --i;
+            }
+            m_nqs.pop_back();
+        }
+    }
+    return m_new_propagation || ctx.inconsistent();
+}
+
+
+bool theory_seq::solve_ne(unsigned idx) {
+    TRACE("seq", display_disequation(tout << "solve: ", m_nqs[idx]););
+    unsigned num_undef_lits = 0;
+    return 
+        (!check_ne_literals(idx, num_undef_lits))
+        || (num_undef_lits <= 1 && propagate_ne2lit(idx))
+        || (num_undef_lits == 0 && propagate_ne2eq(idx))
+        || reduce_ne(idx);
+}
+        
+bool theory_seq::check_ne_literals(unsigned idx, unsigned& num_undef_lits) {
+    ne const& n = m_nqs[idx];
+    context& ctx = get_context();
+    for (literal lit : n.lits()) {
+        switch (ctx.get_assignment(lit)) {
+        case l_false:
+            TRACE("seq", display_disequation(tout << "has false literal\n", n);
+                  ctx.display_literal_verbose(tout, lit);
+                  tout << "\n" << lit << " " << ctx.is_relevant(lit) << "\n";
+                  );
+            return false;
+        case l_true:
+            break;
+        case l_undef:
+            ++num_undef_lits;
+            break;
+        }
+    }
+    return true;
+}
+
+/*
+  \brief propagate if there is a single undefined literal, others are true.
+*/
+
+bool theory_seq::propagate_ne2lit(unsigned idx) {
+    ne const& n = m_nqs[idx];
+    context& ctx = get_context();
+    if (!n.eqs().empty()) {
+        return false;
+    }
+    literal_vector lits;
+    literal undef_lit = null_literal;
+    for (literal lit : n.lits()) {
+        switch (ctx.get_assignment(lit)) {
+        case l_true:
+            lits.push_back(lit);
+            break;
+        case l_false:
+            return true;
+            break;
+        case l_undef:
+            if (undef_lit != null_literal)
+                return false;
+            undef_lit = lit;
+            break;
+        }
+    }
+    if (undef_lit == null_literal) {
+        dependency* dep = n.dep();
+        dependency* dep1 = nullptr;
+        if (explain_eq(n.l(), n.r(), dep1)) {
+            literal diseq = mk_eq(n.l(), n.r(), false);
+            if (ctx.get_assignment(diseq) == l_false) {
+                lits.reset();                
+                lits.push_back(~diseq);
+                dep = dep1;
+                TRACE("seq", tout << "conflict explained\n";);
+            }
+        }
+        set_conflict(dep, lits);
+    }
+    else {
+        TRACE("seq", tout << "propagate: " << undef_lit << "\n";);
+        propagate_lit(n.dep(), lits.size(), lits.c_ptr(), ~undef_lit);
+    }
+    return true;
+}
+
+/*
+  \brief propagate "" != s into s = head(s) + tail(s)
+  Assumes all literals are assigned to true.
+*/
+bool theory_seq::propagate_ne2eq(unsigned idx) {
+    ne const& n = m_nqs[idx];
+    if (n.eqs().size() != 1)
+        return false;
+    auto const& l = n[0].first;
+    auto const& r = n[0].second;
+    if (l.empty()) 
+        return propagate_ne2eq(idx, r);
+    if (r.empty())
+        return propagate_ne2eq(idx, l);
+    return false;
+}
+ 
+bool theory_seq::propagate_ne2eq(unsigned idx, expr_ref_vector const& es) {
+    if (es.empty())
+        return false;
+    ne const& n = m_nqs[idx];
+    expr_ref e(m), head(m), tail(m);
+    e = mk_concat(es, m.get_sort(es[0]));
+    m_sk.decompose(e, head, tail);
+    propagate_eq(n.dep(), n.lits(), e, mk_concat(head, tail), false);
+    return true;
+}
+ 
+bool theory_seq::reduce_ne(unsigned idx) {
+    ne const& n = m_nqs[idx];
+    context& ctx = get_context();
+    bool updated = false;
+    dependency* new_deps = n.dep();
+    vector<decomposed_eq> new_eqs;
+    literal_vector new_lits(n.lits());
+    for (unsigned i = 0; i < n.eqs().size(); ++i) {
+        auto const& p = n[i];
+        expr_ref_vector& ls = m_ls;
+        expr_ref_vector& rs = m_rs;
+        expr_ref_pair_vector& eqs = m_new_eqs;
+        ls.reset(); rs.reset(); eqs.reset();
+        dependency* deps = nullptr;
+        bool change = false;
+        if (!canonize(p.first,  ls, deps, change)) return false;
+        if (!canonize(p.second, rs, deps, change)) return false;
+        new_deps = m_dm.mk_join(deps, new_deps);
+
+        if (!m_seq_rewrite.reduce_eq(ls, rs, eqs, change)) {
+            TRACE("seq", display_disequation(tout << "reduces to false: ", n);
+                  tout << p.first << " -> " << ls << "\n";
+                  tout << p.second << " -> " << rs << "\n";);
+            
+            return true;
+        }
+        
+        if (!change) {
+            TRACE("seq", tout << "no change " << p.first << " " << p.second << "\n";);
+            if (updated) {
+                new_eqs.push_back(p);
+            }
+            continue;
+        }
+
+        if (!updated) {
+            for (unsigned j = 0; j < i; ++j) {
+                new_eqs.push_back(n[j]);
+            }
+            updated = true;
+        }
+        if (!ls.empty() || !rs.empty()) {
+            new_eqs.push_back(decomposed_eq(ls, rs));
+        }
+        TRACE("seq",
+              for (auto const& p : eqs) tout << mk_pp(p.first, m) << " != " << mk_pp(p.second, m) << "\n";
+              for (auto const& p : new_eqs) tout << p.first << " != " << p.second << "\n";
+              tout << p.first << " != " << p.second << "\n";);
+        
+        for (auto const& p : eqs) {
+            expr* nl = p.first;
+            expr* nr = p.second;
+            if (m_util.is_seq(nl) || m_util.is_re(nl)) {
+                ls.reset();
+                rs.reset(); 
+                m_util.str.get_concat_units(nl, ls);
+                m_util.str.get_concat_units(nr, rs);
+                new_eqs.push_back(decomposed_eq(ls, rs));
+            }
+            else if (nl != nr) {                
+                literal lit(mk_eq(nl, nr, false));
+                ctx.mark_as_relevant(lit);
+                new_lits.push_back(lit);
+                switch (ctx.get_assignment(lit)) {
+                case l_false:
+                    return true;
+                case l_true:
+                    break;
+                case l_undef:
+                    m_new_propagation = true;
+                    break;
+                }
+            }
+        }
+    }
+
+
+    TRACE("seq", display_disequation(tout << "updated: " << updated << "\n", n););
+
+    if (updated) {
+        m_nqs.set(idx, ne(n.l(), n.r(), new_eqs, new_lits, new_deps));
+        TRACE("seq", display_disequation(tout << "updated: ", m_nqs[idx]););
+    }
+    return false;
+}
+
+
+bool theory_seq::branch_nqs() {
+   for (unsigned i = 0; i < m_nqs.size(); ++i) {
+       ne n = m_nqs[i];
+       lbool r = branch_nq(n);
+       switch (r) {
+       case l_undef: // needs assignment to a literal.
+           return true;
+       case l_true:  // disequality is satisfied.
+           m_nqs.erase_and_swap(i);
+           break;
+       case l_false: // needs to be expanded.
+           m_nqs.erase_and_swap(i);
+           return true;
+       }
+   }
+   return false;
+}
+
+lbool theory_seq::branch_nq(ne const& n) {
+
+    context& ctx = get_context();
+    literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false);
+    ctx.mark_as_relevant(eq_len);
+    switch (ctx.get_assignment(eq_len)) {
+    case l_false:
+        TRACE("seq", ctx.display_literal_smt2(tout << "lengths are different: ", eq_len) << "\n";);
+        return l_true;
+    case l_undef:
+        return l_undef;
+    default:
+        break;
+    }
+    literal eq = mk_eq(n.l(), n.r(), false);
+    literal len_gt = mk_literal(m_autil.mk_ge(mk_len(n.l()), m_autil.mk_int(1)));
+    ctx.mark_as_relevant(len_gt);
+    switch (ctx.get_assignment(len_gt)) {
+    case l_false:
+        add_axiom(eq, ~eq_len, len_gt);
+        return l_false;
+    case l_undef:
+        return l_undef;
+    default:
+        break;
+    }
+
+    expr_ref h1(m), t1(m), h2(m), t2(m);
+    mk_decompose(n.l(), h1, t1);
+    mk_decompose(n.r(), h2, t2);
+    literal eq_head = mk_eq(h1, h2, false);
+    ctx.mark_as_relevant(eq_head);
+    switch (ctx.get_assignment(eq_head)) {
+    case l_false:
+        TRACE("seq", ctx.display_literal_smt2(tout << "heads are different: ", eq_head) << "\n";);
+        return l_true;
+    case l_undef:
+        return l_undef;
+    default:
+        break;
+    }
+    // l = r or |l| != |r| or |l| > 0
+    // l = r or |l| != |r| or h1 != h2 or t1 != t2
+    add_axiom(eq, ~eq_len, len_gt);
+    add_axiom(eq, ~eq_len, ~eq_head, ~mk_eq(t1, t2, false));
+    return l_false;
+}
+
diff --git a/src/smt/seq_offset_eq.cpp b/src/smt/seq_offset_eq.cpp
new file mode 100644
index 000000000..7c02f611c
--- /dev/null
+++ b/src/smt/seq_offset_eq.cpp
@@ -0,0 +1,133 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    seq_offset_eq.h
+
+Abstract:
+
+    Container for maintaining equalities between lengths of sequences.
+
+Author:
+
+    Thai Minh Trinh 2017
+    Nikolaj Bjorner (nbjorner) 2020-4-16
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "smt/seq_offset_eq.h"
+#include "smt/smt_context.h"
+
+using namespace smt;
+
+/**
+Match:
+  e  == val      where val is an integer
+  e  == r1 - r2
+  r1 == len(e1)
+  r2 == len(e2)
+update m_offset_equalities to contain.
+  r1 |-> [r2 |-> val]
+*/
+
+seq_offset_eq::seq_offset_eq(theory& th, ast_manager& m): 
+    th(th), m(m), seq(m), a(m), m_propagation_level(-1) {
+}
+
+bool seq_offset_eq::match_x_minus_y(expr* e, expr*& x, expr*& y) const {
+    expr* z = nullptr, *u = nullptr;
+    rational fact;
+    return 
+        a.is_add(e, x, z) && 
+        a.is_mul(z, u, y) &&
+        a.is_numeral(u, fact) && 
+        fact.is_minus_one();
+}
+
+
+void seq_offset_eq::len_offset(expr* e, int val) {
+    context & ctx = th.get_context();
+    expr *x = nullptr, *y = nullptr;
+    expr *e1 = nullptr, *e2 = nullptr;
+    if (match_x_minus_y(e, x, y) && 
+        ctx.e_internalized(x) && 
+        ctx.e_internalized(y)) {
+        TRACE("seq", tout << "eqc: " << mk_pp(e, m) << "\n";);    
+        enode* r1 = th.get_root(x);
+        enode* r2 = th.get_root(y);
+        for (enode* n1 : *r1) {
+            if (!seq.str.is_length(n1->get_owner(), e1)) 
+                continue;
+            for (enode* n2 : *r2) {
+                if (!seq.str.is_length(n2->get_owner(), e2)) 
+                    continue;
+                if (r1->get_owner_id() > r2->get_owner_id()) {
+                    std::swap(r1, r2);
+                    val = -val;
+                }
+                m_offset_equalities.insert(r1, r2, val);
+                m_has_offset_equality.insert(r1);
+                m_has_offset_equality.insert(r2);
+                TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";);
+                return;
+            }
+            return;
+        }
+    }
+}
+
+// Find the length offset from the congruence closure core
+void seq_offset_eq::prop_arith_to_len_offset() {
+    rational val;
+    for (enode* n : th.get_context().enodes()) {
+        if (a.is_numeral(n->get_owner(), val) && val.is_int32() && INT_MIN < val.get_int32()) {
+            TRACE("seq", tout << "offset: " << mk_pp(n->get_owner(), m) << "\n";);
+            enode *next = n->get_next();
+            while (next != n) {
+                len_offset(next->get_owner(), val.get_int32());
+                next = next->get_next();
+            }
+        }
+    }
+}
+
+bool seq_offset_eq::find(enode* n1, enode* n2, int& offset) const {
+    n1 = n1->get_root();
+    n2 = n2->get_root();
+    if (n1->get_owner_id() > n2->get_owner_id()) 
+        std::swap(n1, n2);
+    return 
+        !a.is_numeral(n2->get_owner()) && 
+        !a.is_numeral(n2->get_owner()) && 
+        m_offset_equalities.find(n1, n2, offset);
+}
+
+bool seq_offset_eq::contains(enode* r) {
+    r = r->get_root();
+    return !a.is_numeral(r->get_owner()) && m_has_offset_equality.contains(r);
+}
+
+bool seq_offset_eq::propagate() {
+    context& ctx = th.get_context();
+    int lvl = (int) ctx.get_scope_level();
+    if (lvl > m_propagation_level) {
+        m_propagation_level = lvl;
+        prop_arith_to_len_offset();
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+void seq_offset_eq::pop_scope_eh(unsigned num_scopes) {
+    context& ctx = th.get_context();
+    int new_lvl = (int) (ctx.get_scope_level() - num_scopes);
+    if (m_propagation_level > new_lvl) {
+        m_propagation_level = -1;
+        m_offset_equalities.reset();
+        m_has_offset_equality.reset();
+    }
+}
diff --git a/src/smt/seq_offset_eq.h b/src/smt/seq_offset_eq.h
new file mode 100644
index 000000000..e3c138f9e
--- /dev/null
+++ b/src/smt/seq_offset_eq.h
@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    seq_offset_eq.h
+
+Abstract:
+
+    Container for maintaining equalities between lengths of sequences.
+
+Author:
+
+    Thai Minh Trinh 2017
+    Nikolaj Bjorner (nbjorner) 2020-4-16
+
+--*/
+#pragma once
+
+#include "util/obj_pair_hashtable.h"
+#include "ast/seq_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "smt/smt_theory.h"
+
+namespace smt {
+
+    class seq_offset_eq {
+        theory&        th;
+        ast_manager&   m;
+        seq_util       seq;
+        arith_util     a;
+        obj_hashtable<enode>             m_has_offset_equality;
+        obj_pair_map<enode, enode, int>  m_offset_equalities;
+        int                              m_propagation_level;
+
+        bool match_x_minus_y(expr* e, expr*& x, expr*& y) const;
+        void len_offset(expr* e, int val);
+        void prop_arith_to_len_offset();
+
+    public:
+
+        seq_offset_eq(theory& th, ast_manager& m);
+        bool empty() const { return m_offset_equalities.empty(); }
+        /**
+           \breif determine if r1 = r2 + offset
+         */
+        bool find(enode* r1, enode* r2, int& offset) const;
+        bool contains(enode* r1, enode* r2) const { int offset = 0; return find(r1, r2, offset); }
+        bool contains(enode* r);
+        bool propagate();
+        void pop_scope_eh(unsigned num_scopes);
+    };
+
+};
+
diff --git a/src/smt/seq_skolem.cpp b/src/smt/seq_skolem.cpp
index 60595bf7f..d74b3329b 100644
--- a/src/smt/seq_skolem.cpp
+++ b/src/smt/seq_skolem.cpp
@@ -112,6 +112,7 @@ decompose_main:
         head = seq.str.mk_unit(seq.str.mk_nth_i(s, idx));
         tail = mk(m_tail, s, idx);
         m_rewrite(head);
+        m_rewrite(tail);
     }
     else {
         head = seq.str.mk_unit(seq.str.mk_nth_i(e, a.mk_int(0)));
diff --git a/src/smt/seq_skolem.h b/src/smt/seq_skolem.h
index e26368403..5b9065aae 100644
--- a/src/smt/seq_skolem.h
+++ b/src/smt/seq_skolem.h
@@ -92,6 +92,11 @@ namespace smt {
         bool is_step(expr* e) const { return is_skolem(m_aut_step, e); }
         bool is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const;
         bool is_accept(expr* acc) const {  return is_skolem(m_accept, acc); }
+        bool is_accept(expr* a, expr*& s, expr*& i, expr*& r, expr*& n) const { 
+            return is_accept(a) && (s = to_app(a)->get_arg(0), i = to_app(a)->get_arg(1), 
+                                    r = to_app(a)->get_arg(2), n = to_app(a)->get_arg(3), 
+                                    true); 
+        }
         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/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index c13efaac9..81481882e 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -767,7 +767,6 @@ namespace smt {
        if it already exists. Otherwise, return 0 and add p to the todo-list.
     */
     proof * conflict_resolution::get_proof(enode * n1, enode * n2) {
-        SASSERT(n1 != n2);
         proof * pr;
         if (m_eq2proof.find(n1, n2, pr)) {
             TRACE("proof_gen_bug", tout << "eq2_pr_cached: #" << n1->get_owner_id() << " #" << n2->get_owner_id() << "\n";);
@@ -1204,6 +1203,12 @@ namespace smt {
 
     void conflict_resolution::mk_proof(enode * lhs, enode * rhs) {
         SASSERT(!m_eq2proof.contains(lhs, rhs));
+        if (lhs == rhs) {
+            proof* pr = m.mk_reflexivity(lhs->get_owner());
+            m_new_proofs.push_back(pr);
+            m_eq2proof.insert(lhs, rhs, pr);
+            return;
+        }
         enode * c = find_common_ancestor(lhs, rhs);
         ptr_buffer<proof> prs1;
         mk_proof(lhs, c, prs1);
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 58b14c811..1da6a36bd 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -354,6 +354,21 @@ namespace smt {
         enode_vector::const_iterator end_parents() const { 
             return m_parents.end(); 
         }
+
+        class iterator {
+            enode* m_first;
+            enode* m_last;
+        public:
+            iterator(enode* n, enode* m): m_first(n), m_last(m) {} 
+            enode* operator*() { return m_first; }
+            iterator& operator++() { if (!m_last) m_last = m_first; m_first = m_first->m_next; return *this; }
+            iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
+            bool operator==(iterator const& other) const { return m_last == other.m_last && m_first == other.m_first; }
+            bool operator!=(iterator const& other) const { return !(*this == other); }            
+        };
+
+        iterator begin() { return iterator(this, nullptr); }
+        iterator end() { return iterator(this, this); }
         
         theory_var_list const * get_th_var_list() const { 
             return m_th_var_list.get_th_var() == null_theory_var ? nullptr : &m_th_var_list;
diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp
index 9aeed06f6..3eef0ac5f 100644
--- a/src/smt/smt_justification.cpp
+++ b/src/smt/smt_justification.cpp
@@ -177,7 +177,8 @@ namespace smt {
 
 
     void mp_iff_justification::get_antecedents(conflict_resolution & cr) {
-        SASSERT(m_node1 != m_node2);
+        if (m_node1 == m_node2)
+            return;
         cr.mark_eq(m_node1, m_node2);
         context & ctx = cr.get_context();
         bool_var v    = ctx.enode2bool_var(m_node1);
@@ -187,6 +188,9 @@ namespace smt {
     }
 
     proof * mp_iff_justification::mk_proof(conflict_resolution & cr) {
+        ast_manager& m = cr.get_manager();
+        if (m_node1 == m_node2)
+            return m.mk_reflexivity(m_node1->get_owner());
         proof * pr1   = cr.get_proof(m_node1, m_node2);
         context & ctx = cr.get_context();
         bool_var v    = ctx.enode2bool_var(m_node1);
@@ -194,7 +198,7 @@ namespace smt {
         literal l(v, val == l_false);
         proof * pr2   = cr.get_proof(l);
         if (pr1 && pr2) {
-            ast_manager & m = cr.get_manager();
+            
             proof * pr;
             SASSERT(m.has_fact(pr1));
             SASSERT(m.has_fact(pr2));
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 80d07cc56..a1537e99e 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -682,6 +682,7 @@ namespace smt {
         // 
         setup_mi_arith();
         setup_arrays(); 
+        setup_card();
     }
 
     void setup::setup_UFNIA() {
diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index b34a41cff..911d397f2 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -513,6 +513,8 @@ namespace smt {
 
         enode* ensure_enode(expr* e);
 
+        enode* get_root(expr* e) { return ensure_enode(e)->get_root(); }
+
         // -----------------------------------
         //
         // Model generation
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 6de40d87e..3d3b0ddd6 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -182,14 +182,23 @@ template<typename Ext>
 rational theory_arith<Ext>::decompose_monomial(expr* m, buffer<var_power_pair>& vp) const {
     rational coeff(1);
     vp.reset();
+    expr_fast_mark1 mark;
     auto insert = [&](expr* arg) {
         rational r;
         if (m_util.is_numeral(arg, r)) 
             coeff *= r;
-        else if (!vp.empty() && vp.back().first == arg) 
-            vp.back().second += 1;
-        else 
+        else if (mark.is_marked(arg)) {
+            for (unsigned i = vp.size(); i-- > 0; ) {
+                if (vp[i].first == arg) {
+                    vp[i].second++;
+                    break;
+                }
+            }
+        }
+        else {
+            mark.mark(arg);
             vp.push_back(var_power_pair(arg, 1));
+        }
     };
     while (m_util.is_mul(m)) {
         unsigned sz = to_app(m)->get_num_args();
@@ -394,7 +403,8 @@ bool theory_arith<Ext>::update_bounds_using_interval(theory_var v, interval cons
         }
         bound * old_lower = lower(v);
         if (old_lower == nullptr || new_lower > old_lower->get_value()) {
-            TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << new_lower << "\n";
+            TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << mk_pp(var2expr(v), get_manager()) 
+                  << " " << new_lower << "\n";
                   display_interval(tout, i); tout << "\n";);
             mk_derived_nl_bound(v, new_lower, B_LOWER, i.get_lower_dependencies());
             r = true;
@@ -722,19 +732,19 @@ bool theory_arith<Ext>::branch_nl_int_var(theory_var v) {
 */
 template<typename Ext>
 bool theory_arith<Ext>::is_monomial_linear(expr * m) const {
-
     SASSERT(is_pure_monomial(m));
     unsigned num_nl_vars = 0;
     for (expr* arg : *to_app(m)) {
         if (!get_context().e_internalized(arg))
             return false;
         theory_var _var = expr2var(arg);
+        CTRACE("non_linear", is_fixed(_var), 
+               tout << mk_pp(arg, get_manager()) << " is fixed: " << lower_bound(_var) << "\n";);
         if (!is_fixed(_var)) {
             num_nl_vars++;
         }
-        else {
-            if (lower_bound(_var).is_zero())
-                return true;
+        else if (lower_bound(_var).is_zero()) {
+            return true;
         }
     }
     return num_nl_vars <= 1;
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index ddc78a0c1..cfe4522de 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -487,7 +487,7 @@ namespace smt {
                 m_disabled_guards.erase(to_delete);
                 m_enabled_guards.push_back(to_delete);
                 m_q_guards.push_back(to_delete);
-                IF_VERBOSE(1, verbose_stream() << "(smt.recfun :enable-guard)\n");
+                IF_VERBOSE(1, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n");
             }
             else {
                 IF_VERBOSE(1, verbose_stream() << "(smt.recfun :increment-round)\n");
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 2bb9f246f..a184980e2 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -282,9 +282,9 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
     m_lts_checked(false),
     m_eq_id(0),
     m_find(*this),
+    m_offset_eq(*this, m),
     m_overlap(m),
     m_overlap2(m),
-    m_len_prop_lvl(-1),
     m_factory(nullptr),
     m_exclude(m),
     m_axioms(m),
@@ -304,6 +304,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
     m_trail_stack(*this),
     m_ls(m), m_rs(m),
     m_lhs(m), m_rhs(m),
+    m_new_eqs(m),
     m_has_seq(m_util.has_seq()),
     m_res(m),
     m_max_unfolding_depth(1),
@@ -513,7 +514,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
         expr_ref_vector elems(m);
         
         for (unsigned j = 0; j < _lo; ++j) {
-            mk_decompose(seq, head, tail);
+            m_sk.decompose(seq, head, tail);
             elems.push_back(head);
             seq = tail;
         }
@@ -563,9 +564,10 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
     return result;
 }
 
-
 void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
     m_sk.decompose(e, head, tail);
+    add_axiom(~mk_eq_empty(e), mk_eq_empty(tail));;
+    add_axiom(mk_eq_empty(e), mk_eq(e, mk_concat(head, tail), false));
 }
 
 /*
@@ -600,24 +602,24 @@ bool theory_seq::check_extensionality() {
                 if (!canonize(n2->get_owner(), dep, e2)) {
                     return false;
                 }
-                m_lhs.reset(); m_rhs.reset();
+                m_new_eqs.reset();
                 bool change = false;
-                if (!m_seq_rewrite.reduce_eq(e1, e2, m_lhs, m_rhs, change)) {
+                if (!m_seq_rewrite.reduce_eq(e1, e2, m_new_eqs, change)) {
                     TRACE("seq", tout << "exclude " << mk_pp(o1, m) << " " << mk_pp(o2, m) << "\n";);
                     m_exclude.update(o1, o2);
                     continue;
                 }
                 bool excluded = false;
-                for (unsigned j = 0; !excluded && j < m_lhs.size(); ++j) {
-                    if (m_exclude.contains(m_lhs.get(j), m_rhs.get(j))) {
-                        TRACE("seq", tout << "excluded " << j << " " << m_lhs << " " << m_rhs << "\n";);
+                for (auto const& p : m_new_eqs) {
+                    if (m_exclude.contains(p.first, p.second)) {
+                        TRACE("seq", tout << "excluded " << mk_pp(p.first, m) << " " << mk_pp(p.second, m) << "\n";);
                         excluded = true;
+                        break;
                     }
                 }
                 if (excluded) {
                     continue;
                 }
-                TRACE("seq", tout << m_lhs << " = " << m_rhs << "\n";);
                 ctx.assume_eq(n1, n2);
                 return false;
             }
@@ -634,12 +636,7 @@ bool theory_seq::check_contains() {
     context & ctx = get_context();
     for (unsigned i = 0; !ctx.inconsistent() && i < m_ncs.size(); ++i) {
         if (solve_nc(i)) {
-            if (i + 1 != m_ncs.size()) {
-                nc n = m_ncs[m_ncs.size()-1];
-                m_ncs.set(i, n);
-                --i;
-            }
-            m_ncs.pop_back();
+            m_ncs.erase_and_swap(i--);
         }
     }
     return m_new_propagation || ctx.inconsistent();
@@ -907,14 +904,15 @@ bool theory_seq::lift_ite(expr_ref_vector const& ls, expr_ref_vector const& rs,
 
 bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependency* deps) {
     context& ctx = get_context();
-    expr_ref_vector lhs(m), rhs(m);
+    expr_ref_pair_vector& new_eqs = m_new_eqs;
+    new_eqs.reset();
     bool changed = false;
     TRACE("seq", 
           for (expr* l : ls) tout << "s#" << l->get_id() << " " << mk_bounded_pp(l, m, 2) << "\n";
           tout << " = \n";
           for (expr* r : rs) tout << "s#" << r->get_id() << " " << mk_bounded_pp(r, m, 2) << "\n";);
 
-    if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, changed)) {
+    if (!m_seq_rewrite.reduce_eq(ls, rs, new_eqs, changed)) {
         // equality is inconsistent.
         TRACE("seq_verbose", tout << ls << " != " << rs << "\n";);
         set_conflict(deps);
@@ -922,27 +920,29 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
     }
 
     if (!changed) {
-        SASSERT(lhs.empty() && rhs.empty());
+        SASSERT(new_eqs.empty());
         return false;
     }
     TRACE("seq",
           tout << "reduced to\n";
-          for (expr* l : lhs) tout << mk_bounded_pp(l, m, 2) << "\n";
-          tout << " = \n";
-          for (expr* r : rhs) tout << mk_bounded_pp(r, m, 2) << "\n";
+          for (auto p : new_eqs) {
+              tout << mk_bounded_pp(p.first, m, 2) << "\n";
+              tout << " = \n";
+              tout << mk_bounded_pp(p.second, m, 2) << "\n";
+          }
           );
-    SASSERT(lhs.size() == rhs.size());
-    m_seq_rewrite.add_seqs(ls, rs, lhs, rhs);
-    if (lhs.empty()) {
+    m_seq_rewrite.add_seqs(ls, rs, new_eqs);
+    if (new_eqs.empty()) {
         TRACE("seq", tout << "solved\n";);
         return true;
     }
     TRACE("seq_verbose", 
-          tout << ls << " = " << rs << "\n";
-          tout << lhs << " = " << rhs << "\n";);
-    for (unsigned i = 0; !ctx.inconsistent() && i < lhs.size(); ++i) {
-        expr_ref li(lhs.get(i), m);
-        expr_ref ri(rhs.get(i), m);
+          tout << ls << " = " << rs << "\n";);
+    for (auto const& p : new_eqs) {
+        if (ctx.inconsistent())
+            break;
+        expr_ref li(p.first, m);
+        expr_ref ri(p.second, m);
         if (solve_unit_eq(li, ri, deps)) {
             // no-op
         }
@@ -956,8 +956,8 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
     }
     TRACE("seq_verbose",
           if (!ls.empty() || !rs.empty()) tout << ls << " = " << rs << ";\n";
-          for (unsigned i = 0; i < lhs.size(); ++i) {
-              tout << mk_pp(lhs.get(i), m) << " = " << mk_pp(rhs.get(i), m) << ";\n";
+          for (auto const& p : new_eqs) {
+              tout << mk_pp(p.first, m) << " = " << mk_pp(p.second, m) << ";\n";
           });
 
 
@@ -976,7 +976,7 @@ bool theory_seq::solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs
 
 bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep) {
     if (rs.empty()) {
-        literal lit = mk_simplified_literal(m_autil.mk_le(n, m_autil.mk_int(-1)));
+        literal lit = m_ax.mk_le(n, -1);
         propagate_lit(dep, 0, nullptr, lit);
         return true;
     }
@@ -1003,7 +1003,7 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep)
     if (rs.size() > 1) {
         VERIFY (m_util.str.is_unit(rs[0], u));
         digit = m_sk.mk_digit2int(u);
-        propagate_lit(dep, 0, nullptr, mk_simplified_literal(m_autil.mk_ge(digit, m_autil.mk_int(1))));
+        propagate_lit(dep, 0, nullptr, m_ax.mk_ge(digit, 1));
     }
     return true;
 }
@@ -1060,7 +1060,7 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
     }
     rational hi;
     if (m_sk.is_tail_u(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) {
-        propagate_lit(deps, 0, nullptr, mk_literal(m_autil.mk_le(mk_len(s), m_autil.mk_int(idx+1))));
+        propagate_lit(deps, 0, nullptr, m_ax.mk_le(mk_len(s), idx+1));
         return true;
     }
     return false;
@@ -1196,15 +1196,14 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
     expr* s, *i, *l;
     rational r;
     if (m_util.str.is_extract(e, s, i, l)) {
-        // 0 <= i <= len(s), 0 <= l, i + l <= len(s)
-        expr_ref zero(m_autil.mk_int(0), m);        
+        // 0 <= i <= len(s), 0 <= l, i + l <= len(s)       
         expr_ref ls = mk_len(s);
         expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
         bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
-        literal i_ge_0 = i_is_zero?true_literal:mk_simplified_literal(m_autil.mk_ge(i, zero));
-        literal i_lt_len_s = ~mk_simplified_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
-        literal li_ge_ls  = mk_simplified_literal(m_autil.mk_ge(ls_minus_i_l, zero));
-        literal l_ge_zero = mk_simplified_literal(m_autil.mk_ge(l, zero));
+        literal i_ge_0 = i_is_zero?true_literal:m_ax.mk_ge(i, 0);
+        literal i_lt_len_s = ~m_ax.mk_ge(mk_sub(i, ls), 0);
+        literal li_ge_ls  = m_ax.mk_ge(ls_minus_i_l, 0);
+        literal l_ge_zero = m_ax.mk_ge(l, 0);
         literal _lits[4] = { i_ge_0, i_lt_len_s, li_ge_ls, l_ge_zero };
         if (ctx.get_assignment(i_ge_0) == l_true &&
             ctx.get_assignment(i_lt_len_s) == l_true && 
@@ -1219,10 +1218,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
     }
     else if (m_util.str.is_at(e, s, i)) {
         // has length 1 if 0 <= i < len(s)
-        expr_ref zero(m_autil.mk_int(0), m);
         bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
-        literal i_ge_0 = i_is_zero?true_literal:mk_simplified_literal(m_autil.mk_ge(i, zero));
-        literal i_lt_len_s = ~mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
+        literal i_ge_0 = i_is_zero?true_literal:m_ax.mk_ge(i, 0);
+        literal i_lt_len_s = ~m_ax.mk_ge(mk_sub(i, mk_len(s)), 0);
         literal _lits[2] = { i_ge_0, i_lt_len_s};
         if (ctx.get_assignment(i_ge_0) == l_true &&
             ctx.get_assignment(i_lt_len_s) == l_true) {
@@ -1233,10 +1231,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
         }
     }
     else if (m_sk.is_pre(e, s, i)) {
-        expr_ref zero(m_autil.mk_int(0), m);
         bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
-        literal i_ge_0 = i_is_zero?true_literal:mk_simplified_literal(m_autil.mk_ge(i, zero));
-        literal i_lt_len_s = ~mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
+        literal i_ge_0 = i_is_zero?true_literal:m_ax.mk_ge(i, 0);
+        literal i_lt_len_s = ~m_ax.mk_ge(mk_sub(i, mk_len(s)), 0);
         literal _lits[2] = { i_ge_0, i_lt_len_s };
         if (ctx.get_assignment(i_ge_0) == l_true &&
             ctx.get_assignment(i_lt_len_s) == l_true) {
@@ -1247,9 +1244,8 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
         }
     }
     else if (m_sk.is_post(e, s, i)) {
-        expr_ref zero(m_autil.mk_int(0), m);
-        literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
-        literal len_s_ge_i = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(s), i), zero));
+        literal i_ge_0 = m_ax.mk_ge(i, 0);
+        literal len_s_ge_i = m_ax.mk_ge(mk_sub(mk_len(s), i), 0);
         literal _lits[2] = { i_ge_0, len_s_ge_i };
         if (ctx.get_assignment(i_ge_0) == l_true && 
             ctx.get_assignment(len_s_ge_i) == l_true) {
@@ -1264,7 +1260,7 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
         // e = tail(s, l), len(s) <= l => len(tail(s, l)) = 0
 
         expr_ref len_s = mk_len(s);
-        literal len_s_gt_l = mk_simplified_literal(m_autil.mk_ge(mk_sub(len_s, l), m_autil.mk_int(1)));
+        literal len_s_gt_l = m_ax.mk_ge(mk_sub(len_s, l), 1);
         switch (ctx.get_assignment(len_s_gt_l)) {
         case l_true:
             len = mk_sub(mk_sub(len_s, l), m_autil.mk_int(1));
@@ -1288,248 +1284,6 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
 }
 
 
-bool theory_seq::branch_nqs() {
-   for (unsigned i = 0; i < m_nqs.size(); ++i) {
-       ne n = m_nqs[i];
-       lbool r = branch_nq(n);
-       switch (r) {
-       case l_undef: // needs assignment to a literal.
-           return true;
-       case l_true:  // disequality is satisfied.
-           break;
-       case l_false: // needs to be expanded.
-           if (m_nqs.size() > 1) {
-               ne n2 = m_nqs[m_nqs.size() - 1];
-               m_nqs.set(0, n2);
-           }
-           m_nqs.pop_back();           
-           return true;
-       }
-   }
-   return false;
-}
-
-lbool theory_seq::branch_nq(ne const& n) {
-    context& ctx = get_context();
-    literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false);
-    ctx.mark_as_relevant(eq_len);
-    switch (ctx.get_assignment(eq_len)) {
-    case l_false:
-        TRACE("seq", ctx.display_literal_smt2(tout << "lengths are different: ", eq_len) << "\n";);
-        return l_true;
-    case l_undef:
-        return l_undef;
-    default:
-        break;
-    }
-    literal eq = mk_eq(n.l(), n.r(), false);
-    literal len_gt = mk_literal(m_autil.mk_ge(mk_len(n.l()), m_autil.mk_int(1)));
-    ctx.mark_as_relevant(len_gt);
-    switch (ctx.get_assignment(len_gt)) {
-    case l_false:
-        add_axiom(eq, ~eq_len, len_gt);
-        return l_false;
-    case l_undef:
-        return l_undef;
-    default:
-        break;
-    }
-    expr_ref h1(m), t1(m), h2(m), t2(m);
-    mk_decompose(n.l(), h1, t1);
-    mk_decompose(n.r(), h2, t2);
-    literal eq_head = mk_eq(h1, h2, false);
-    ctx.mark_as_relevant(eq_head);
-    switch (ctx.get_assignment(eq_head)) {
-    case l_false:
-        TRACE("seq", ctx.display_literal_smt2(tout << "heads are different: ", eq_head) << "\n";);
-        return l_true;
-    case l_undef:
-        return l_undef;
-    default:
-        break;
-    }
-    // l = r or |l| != |r| or |l| > 0
-    // l = r or |l| != |r| or h1 != h2 or t1 != t2
-    add_axiom(eq, ~eq_len, len_gt);
-    add_axiom(eq, ~eq_len, ~eq_head, ~mk_eq(t1, t2, false));
-    return l_false;
-}
-
-bool theory_seq::solve_nqs(unsigned i) {
-    context & ctx = get_context();
-    for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
-        if (solve_ne(i)) {
-            if (i + 1 != m_nqs.size()) {
-                ne n = m_nqs[m_nqs.size()-1];
-                m_nqs.set(i, n);
-                --i;
-            }
-            m_nqs.pop_back();
-        }
-    }
-    return m_new_propagation || ctx.inconsistent();
-}
-
-
-bool theory_seq::solve_ne(unsigned idx) {
-    context& ctx = get_context();
-    ne const& n = m_nqs[idx];
-
-    TRACE("seq", display_disequation(tout << "solve: ", n););
-
-    unsigned num_undef_lits = 0;
-    for (literal lit : n.lits()) {
-        switch (ctx.get_assignment(lit)) {
-        case l_false:
-            TRACE("seq", display_disequation(tout << "has false literal\n", n);
-                  ctx.display_literal_verbose(tout, lit);
-                  tout << "\n" << lit << " " << ctx.is_relevant(lit) << "\n";
-                  );
-            return true;
-        case l_true:
-            break;
-        case l_undef:
-            ++num_undef_lits;
-            break;
-        }
-    }
-
-    bool updated = false;
-    dependency* new_deps = n.dep();
-    vector<expr_ref_vector> new_ls, new_rs;
-    literal_vector new_lits(n.lits());
-    for (unsigned i = 0; i < n.ls().size(); ++i) {
-        expr_ref_vector& ls = m_ls;
-        expr_ref_vector& rs = m_rs;
-        expr_ref_vector& lhs = m_lhs;
-        expr_ref_vector& rhs = m_rhs;
-        ls.reset(); rs.reset(); lhs.reset(); rhs.reset();
-        dependency* deps = nullptr;
-        bool change = false;
-        if (!canonize(n.ls(i), ls, deps, change)) return false;
-        if (!canonize(n.rs(i), rs, deps, change)) return false;
-
-        if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, change)) {
-            TRACE("seq", display_disequation(tout << "reduces to false: ", n);
-                  tout << n.ls(i) << " -> " << ls << "\n";
-                  tout << n.rs(i) << " -> " << rs << "\n";);
-            
-            return true;
-        }
-        else if (!change) {
-            TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";);
-            if (updated) {
-                new_ls.push_back(n.ls(i));
-                new_rs.push_back(n.rs(i));
-            }
-            continue;
-        }
-        else {
-            if (!updated) {
-                for (unsigned j = 0; j < i; ++j) {
-                    new_ls.push_back(n.ls(j));
-                    new_rs.push_back(n.rs(j));
-                }
-            }
-            updated = true;
-            if (!ls.empty() || !rs.empty()) {
-                new_ls.push_back(ls);
-                new_rs.push_back(rs);
-            }
-            TRACE("seq",
-                  tout << lhs << " != " << rhs << "\n";
-                  for (unsigned j = 0; j < new_ls.size(); ++j) tout << new_ls[j] << " != " << new_rs[j] << "\n";
-                  tout << n.ls(i) << " != " << n.rs(i) << "\n";);
-
-            for (unsigned j = 0; j < lhs.size(); ++j) {
-                expr* nl = lhs[j].get();
-                expr* nr = rhs[j].get();
-                if (m_util.is_seq(nl) || m_util.is_re(nl)) {
-                    ls.reset();
-                    rs.reset(); 
-                    m_util.str.get_concat_units(nl, ls);
-                    m_util.str.get_concat_units(nr, rs);
-                    new_ls.push_back(ls);
-                    new_rs.push_back(rs);
-                }
-                else if (nl != nr) {                
-                    literal lit(mk_eq(nl, nr, false));
-                    ctx.mark_as_relevant(lit);
-                    new_lits.push_back(lit);
-                    switch (ctx.get_assignment(lit)) {
-                    case l_false:
-                        return true;
-                    case l_true:
-                        break;
-                    case l_undef:
-                        ++num_undef_lits;
-                        m_new_propagation = true;
-                        break;
-                    }
-                }
-            }
-            new_deps = m_dm.mk_join(deps, new_deps);
-        }
-    }
-
-    TRACE("seq", display_disequation(tout << "updated: " << updated << " undef lits: " << num_undef_lits << "\n", n););
-
-    if (!updated && num_undef_lits == 0) {
-        return false;
-    }
-    if (!updated) {
-        for (unsigned j = 0; j < n.ls().size(); ++j) {
-            new_ls.push_back(n.ls(j));
-            new_rs.push_back(n.rs(j));
-        }
-    }
-
-    if (num_undef_lits == 1 && new_ls.empty()) {
-        literal_vector lits;
-        literal undef_lit = null_literal;
-        for (literal lit : new_lits) {
-            switch (ctx.get_assignment(lit)) {
-            case l_true:
-                lits.push_back(lit);
-                break;
-            case l_false:
-                UNREACHABLE();
-                break;
-            case l_undef:
-                SASSERT(undef_lit == null_literal);
-                undef_lit = lit;
-                break;
-            }
-        }
-        TRACE("seq", tout << "propagate: " << undef_lit << "\n";);
-        SASSERT(undef_lit != null_literal);
-        propagate_lit(new_deps, lits.size(), lits.c_ptr(), ~undef_lit);
-        return true;
-    }
-    if (updated) {
-        if (num_undef_lits == 0 && new_ls.empty()) {
-            TRACE("seq", tout << "conflict\n";);
-
-            dependency* deps1 = nullptr;
-            if (explain_eq(n.l(), n.r(), deps1)) {
-                literal diseq = mk_eq(n.l(), n.r(), false);
-                if (ctx.get_assignment(diseq) == l_false) {
-                    new_lits.reset();                
-                    new_lits.push_back(~diseq);
-                    new_deps = deps1;
-                    TRACE("seq", tout << "conflict explained\n";);
-                }
-            }
-            set_conflict(new_deps, new_lits);
-            SASSERT(m_new_propagation);
-        }
-        else {
-            m_nqs.push_back(ne(n.l(), n.r(), new_ls, new_rs, new_lits, new_deps));
-            TRACE("seq", display_disequation(tout << "updated: ", m_nqs[m_nqs.size()-1]););
-        }
-    }    
-    return updated;
-}
 
 
 bool theory_seq::solve_nc(unsigned idx) {
@@ -1540,7 +1294,6 @@ bool theory_seq::solve_nc(unsigned idx) {
 #if 1
     expr* a = nullptr, *b = nullptr;
     VERIFY(m_util.str.is_contains(n.contains(), a, b));
-    expr_ref head(m), tail(m);
     literal pre, cnt, ctail, emp;
     lbool is_gt = ctx.get_assignment(len_gt);
     TRACE("seq", ctx.display_literal_smt2(tout << len_gt << " := " << is_gt << "\n", len_gt) << "\n";);
@@ -1582,18 +1335,7 @@ bool theory_seq::solve_nc(unsigned idx) {
     }
     IF_VERBOSE(0, verbose_stream() << n.contains() << "\n");
 #endif    
-    mk_decompose(a, head, tail);
-    expr_ref pref(m_util.str.mk_prefix(b, a), m);
-    expr_ref postf(m_util.str.mk_contains(tail, b), m);
-    m_rewrite(pref);
-    m_rewrite(postf);
-    pre = mk_literal(pref);
-    cnt = mk_literal(n.contains());
-    ctail = mk_literal(postf);
-    emp = mk_literal(m_util.str.mk_is_empty(a));
-    add_axiom(cnt, ~pre);
-    add_axiom(cnt, ~ctail);
-    add_axiom(emp, mk_eq(a, m_util.str.mk_concat(head, tail), false));
+    m_ax.unroll_not_contains(n.contains());
     return true;
     
 #endif    
@@ -1983,12 +1725,12 @@ std::ostream& theory_seq::display_disequation(std::ostream& out, ne const& e) co
     if (!e.lits().empty()) {
         out << "\n";
     }
-    for (unsigned j = 0; j < e.ls().size(); ++j) {
-        for (expr* t : e.ls(j)) {
+    for (unsigned j = 0; j < e.eqs().size(); ++j) {
+        for (expr* t : e[j].first) {
             out << mk_bounded_pp(t, m, 2) << " ";
         }
         out << " != ";
-        for (expr* t : e.rs(j)) {
+        for (expr* t : e[j].second) {
             out << mk_bounded_pp(t, m, 2) << " ";
         }
         out << "\n";
@@ -2088,9 +1830,9 @@ void theory_seq::init_model(model_generator & mg) {
         m_factory->register_value(n.r());  
     }
     for (ne const& n : m_nqs) {
-        for (unsigned i = 0; i < n.ls().size(); ++i) {
-            init_model(n.ls(i));
-            init_model(n.rs(i));
+        for (unsigned i = 0; i < n.eqs().size(); ++i) {
+            init_model(n[i].first);
+            init_model(n[i].second);
         }
     }
 }
@@ -2308,8 +2050,9 @@ void theory_seq::validate_model(model& mdl) {
     for (auto const& eq : m_eqs) {
         expr_ref_vector ls = eq.ls();
         expr_ref_vector rs = eq.rs();
-        expr_ref l(m_util.str.mk_concat(ls), m);
-        expr_ref r(m_util.str.mk_concat(rs), m);
+        sort* srt = m.get_sort(ls.get(0));
+        expr_ref l(m_util.str.mk_concat(ls, srt), m);
+        expr_ref r(m_util.str.mk_concat(rs, srt), m);
         if (!mdl.are_equal(l, r)) {
             IF_VERBOSE(0, verbose_stream() << "equality failed: " << l << " = " << r << "\nbut\n" << mdl(l) << " != " << mdl(r) << "\n");
         }
@@ -3071,7 +2814,7 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
 
     expr* s2 = s;
     for (unsigned j = 0; j <= _idx; ++j) {
-        mk_decompose(s2, head, tail);
+        m_sk.decompose(s2, head, tail);
         elems.push_back(head);
         len1 = mk_len(s2);
         len2 = m_autil.mk_add(m_autil.mk_int(1), mk_len(tail));
@@ -3257,8 +3000,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             propagate_non_empty(lit, e2);
             dependency* dep = m_dm.mk_leaf(assumption(lit));
             // |e1| - |e2| <= -1
-            literal len_gt = mk_simplified_literal(m_autil.mk_le(mk_sub(mk_len(e1), mk_len(e2)), 
-                                                                 m_autil.mk_int(-1)));
+            literal len_gt = m_ax.mk_le(mk_sub(mk_len(e1), mk_len(e2)), -1);
             ctx.force_phase(len_gt);
             m_ncs.push_back(nc(expr_ref(e, m), len_gt, dep));
         }
@@ -3330,7 +3072,6 @@ lbool theory_seq::regex_are_equal(expr* _r1, expr* _r2) {
     m_rewrite(diff);
     eautomaton* aut = get_automaton(diff);
     if (!aut) {
-        std::cout << diff << "\n";
         return l_undef;
     }
     else if (aut->is_empty()) {
@@ -3449,10 +3190,7 @@ 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();
-    }
+    m_offset_eq.pop_scope_eh(num_scopes);
 }
 
 void theory_seq::restart_eh() {
@@ -3513,13 +3251,11 @@ literal theory_seq::mk_accept(expr* s, expr* idx, expr* re, expr* state) {
 }
 
 bool theory_seq::is_accept(expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
-    if (is_accept(e)) {
+    expr* n = nullptr;
+    if (m_sk.is_accept(e, s, idx, re, n)) {
         rational r;
-        s  = to_app(e)->get_arg(0);
-        idx = to_app(e)->get_arg(1);
-        re = to_app(e)->get_arg(2);
         TRACE("seq", tout << mk_pp(re, m) << "\n";);
-        VERIFY(m_autil.is_numeral(to_app(e)->get_arg(3), r));
+        VERIFY(m_autil.is_numeral(n, r));
         SASSERT(r.is_unsigned());
         i = r.get_unsigned();
         aut = get_automaton(re);        
@@ -3550,7 +3286,7 @@ void theory_seq::propagate_step(literal lit, expr* step) {
         // skip
     }
     else {
-        propagate_lit(nullptr, 1, &lit, ~mk_literal(m_autil.mk_le(len_s, idx)));
+        propagate_lit(nullptr, 1, &lit, ~m_ax.mk_le(len_s, _idx));
     }
     ensure_nth(lit, s, idx);
 
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 00c2ec172..f09d6b89a 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -33,6 +33,7 @@ Revision History:
 #include "smt/theory_seq_empty.h"
 #include "smt/seq_skolem.h"
 #include "smt/seq_axioms.h"
+#include "smt/seq_offset_eq.h"
 
 namespace smt {
 
@@ -178,9 +179,12 @@ namespace smt {
             return eq(m_eq_id++, ls, rs, dep);
         }        
 
+        // equalities that are decomposed by conacatenations
+        typedef std::pair<expr_ref_vector, expr_ref_vector> decomposed_eq;
+
         class ne {      
             expr_ref                 m_l, m_r;
-            vector<expr_ref_vector>  m_lhs, m_rhs;
+            vector<decomposed_eq>    m_eqs;
             literal_vector           m_lits;
             dependency*              m_dep;
         public:
@@ -188,36 +192,34 @@ namespace smt {
                 m_l(l), m_r(r), m_dep(dep) {
                     expr_ref_vector ls(l.get_manager()); ls.push_back(l);
                     expr_ref_vector rs(r.get_manager()); rs.push_back(r);
-                    m_lhs.push_back(ls);
-                    m_rhs.push_back(rs);
+                    m_eqs.push_back(std::make_pair(ls, rs));
                 }
 
-            ne(expr_ref const& _l, expr_ref const& _r, vector<expr_ref_vector> const& l, vector<expr_ref_vector> const& r, literal_vector const& lits, dependency* dep):
+            ne(expr_ref const& _l, expr_ref const& _r, vector<decomposed_eq> const& eqs, literal_vector const& lits, dependency* dep):
                 m_l(_l), m_r(_r),
-                m_lhs(l),
-                m_rhs(r),
+                m_eqs(eqs),
                 m_lits(lits),
-                m_dep(dep) {}
+                m_dep(dep) {
+                }
 
             ne(ne const& other): 
                 m_l(other.m_l), m_r(other.m_r),
-                m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
+                m_eqs(other.m_eqs), 
+                m_lits(other.m_lits), m_dep(other.m_dep) {}
 
             ne& operator=(ne const& other) { 
                 if (this != &other) {
                     m_l = other.m_l;
                     m_r = other.m_r;
-                    m_lhs.reset();  m_lhs.append(other.m_lhs);
-                    m_rhs.reset();  m_rhs.append(other.m_rhs); 
+                    m_eqs.reset();  m_eqs.append(other.m_eqs);
                     m_lits.reset(); m_lits.append(other.m_lits); 
                     m_dep = other.m_dep; 
                 }
                 return *this; 
             }            
-            vector<expr_ref_vector> const& ls() const { return m_lhs; }
-            vector<expr_ref_vector> const& rs() const { return m_rhs; }
-            expr_ref_vector const& ls(unsigned i) const { return m_lhs[i]; }
-            expr_ref_vector const& rs(unsigned i) const { return m_rhs[i]; }
+            vector<decomposed_eq> const& eqs() const { return m_eqs; }
+            decomposed_eq const& operator[](unsigned i) const { return m_eqs[i]; }
+
             literal_vector const& lits() const { return m_lits; }
             literal lits(unsigned i) const { return m_lits[i]; }
             dependency* dep() const { return m_dep; }
@@ -334,7 +336,6 @@ namespace smt {
             }
         };
 
-
         struct s_in_re {
             literal     m_lit;
             expr*       m_s;
@@ -377,11 +378,11 @@ namespace smt {
         bool                       m_lts_checked; 
         unsigned                   m_eq_id;
         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_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.
@@ -408,6 +409,7 @@ namespace smt {
         stats            m_stats;
         ptr_vector<expr> m_todo, m_concat;
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
+        expr_ref_pair_vector m_new_eqs;
         bool             m_has_seq;
 
         // maintain automata with regular expressions.
@@ -457,8 +459,6 @@ namespace smt {
         app* get_ite_value(expr* a);
         void get_ite_concat(ptr_vector<expr>& head, ptr_vector<expr>& tail);
         
-        void len_offset(expr* e, rational val);
-        void prop_arith_to_len_offset();
         int find_fst_non_empty_idx(expr_ref_vector const& x);
         expr* find_fst_non_empty_var(expr_ref_vector const& x);
         void find_max_eq_len(expr_ref_vector const& ls, expr_ref_vector const& rs);
@@ -486,11 +486,13 @@ namespace smt {
         void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
         bool branch_variable_eq(eq const& e);
         bool branch_binary_variable(eq const& e);
-        bool eq_unit(expr* const& l, expr* const &r) const;       
+        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* 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 const& indexes, expr_ref_vector const& xs, expr* const& x, expr* const& y1, expr_ref_vector const& ys, expr* const& y2);
+        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 branch_quat_variable(eq const& e);
@@ -508,7 +510,7 @@ namespace smt {
         bool check_contains();
         bool check_lts();
         bool solve_eqs(unsigned start);
-        bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep, unsigned idx);
+        bool solve_eq(unsigned idx);
         bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
         bool lift_ite(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool solve_unit_eq(expr* l, expr* r, dependency* dep);
@@ -530,15 +532,21 @@ namespace smt {
         bool reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps);
 
         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 expr_ref(m_util.str.mk_concat(es.size(), es.c_ptr()), m); }
-        expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr()); }
+        expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es, m.get_sort(es[0])), m); }
+        expr_ref mk_concat(unsigned n, expr*const* es, sort* s) { return expr_ref(m_util.str.mk_concat(n, es, s), m); }
+        expr_ref mk_concat(expr_ref_vector const& es, sort* s) { return mk_concat(es.size(), es.c_ptr(), s); }
+        expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty());  return expr_ref(m_util.str.mk_concat(es.size(), es.c_ptr(), m.get_sort(es[0])), m); }
+        expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr(), m.get_sort(es[0])); }
         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); }
         bool solve_nqs(unsigned i);
         bool solve_ne(unsigned i);
         bool solve_nc(unsigned i);
+        bool check_ne_literals(unsigned idx, unsigned& num_undef_lits);
+        bool propagate_ne2lit(unsigned idx);
+        bool propagate_ne2eq(unsigned idx);
+        bool propagate_ne2eq(unsigned idx, expr_ref_vector const& es);
+        bool reduce_ne(unsigned idx);
         bool branch_nqs();
         lbool branch_nq(ne const& n);
 
@@ -628,7 +636,6 @@ namespace smt {
         expr_ref mk_sub(expr* a, expr* b);
         expr_ref mk_add(expr* a, expr* b);
         expr_ref mk_len(expr* s);
-        enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
         dependency* mk_join(dependency* deps, literal lit);
         dependency* mk_join(dependency* deps, literal_vector const& lits);
 
diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp
index 0cc19a806..dc59f7bb8 100644
--- a/src/tactic/bv/bvarray2uf_tactic.cpp
+++ b/src/tactic/bv/bvarray2uf_tactic.cpp
@@ -30,8 +30,6 @@ class bvarray2uf_tactic : public tactic {
 
     struct imp {
         ast_manager &       m_manager;
-        bool                m_produce_models;
-        bool                m_produce_proofs;
         bool                m_produce_cores;
         bvarray2uf_rewriter m_rw;
 
@@ -39,8 +37,6 @@ class bvarray2uf_tactic : public tactic {
 
         imp(ast_manager & m, params_ref const & p) :
             m_manager(m),
-            m_produce_models(false),
-            m_produce_proofs(false),
             m_produce_cores(false),
             m_rw(m, p) {
             updt_params(p);
@@ -59,10 +55,11 @@ class bvarray2uf_tactic : public tactic {
             result.reset();
             fail_if_unsat_core_generation("bvarray2uf", g);
 
-            m_produce_models = g->models_enabled();
+            bool produce_models = g->models_enabled();
+            bool produce_proofs = g->proofs_enabled();
             model_converter_ref mc;
 
-            if (m_produce_models) {
+            if (produce_models) {
                 generic_model_converter * fmc = alloc(generic_model_converter, m_manager, "bvarray2uf");
                 mc = fmc;
                 m_rw.set_mcs(fmc);
@@ -76,17 +73,17 @@ class bvarray2uf_tactic : public tactic {
             for (unsigned idx = 0; idx < size; idx++) {
                 if (g->inconsistent())
                     break;
-                expr * curr = g->form(idx);
+                expr* curr = g->form(idx);
                 m_rw(curr, new_curr, new_pr);
-                if (m_produce_proofs) {
+                if (produce_proofs) {
                     proof * pr = g->pr(idx);
                     new_pr = m_manager.mk_modus_ponens(pr, new_pr);
                 }
                 g->update(idx, new_curr, new_pr, g->dep(idx));
             }
 
-            for (unsigned i = 0; i < m_rw.m_cfg.extra_assertions.size(); i++)
-                g->assert_expr(m_rw.m_cfg.extra_assertions[i].get());
+            for (expr* a : m_rw.m_cfg.extra_assertions)
+                g->assert_expr(a);
 
             g->inc_depth();
             g->add(mc.get());
diff --git a/src/util/ref_pair_vector.h b/src/util/ref_pair_vector.h
new file mode 100644
index 000000000..706eb5a6a
--- /dev/null
+++ b/src/util/ref_pair_vector.h
@@ -0,0 +1,278 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    ref_pair_vector.h
+
+Abstract:
+
+    Vector of pairs of smart pointers.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-01-04.
+
+Revision History:
+
+--*/
+#pragma once
+
+#include "util/vector.h"
+#include "util/obj_ref.h"
+#include "util/ref_vector.h"
+
+/**
+   \brief Vector of smart pointers.
+   Ref must provided the methods
+   - void dec_ref(T * obj)
+   - void inc_ref(T * obj)
+*/
+template<typename T, typename Ref>
+class ref_pair_vector_core : public Ref {
+protected:
+    svector<std::pair<T*,T*>> m_nodes;
+    typedef std::pair<T*,T*> elem_t;
+    
+    void inc_ref(T * o) { Ref::inc_ref(o); }
+    void dec_ref(T * o) { Ref::dec_ref(o); }
+    void inc_ref(elem_t const& p) { inc_ref(p.first); inc_ref(p.second); }
+    void dec_ref(elem_t const& p) { dec_ref(p.first); dec_ref(p.second); }
+
+    void dec_range_ref(elem_t const * begin, elem_t const * end) {
+        for (auto it = begin; it < end; ++it)
+            dec_ref(*it);
+    }
+
+public:
+    typedef T * data;
+
+    ref_pair_vector_core(Ref const & r = Ref()):Ref(r) {}
+
+    ref_pair_vector_core(ref_pair_vector_core && other) :
+        Ref(std::move(other)),
+        m_nodes(std::move(other.m_nodes)) {}
+    
+    ~ref_pair_vector_core() {
+        dec_range_ref(m_nodes.begin(), m_nodes.end());
+    }
+    
+    void reset() {
+        dec_range_ref(m_nodes.begin(), m_nodes.end());
+        m_nodes.reset();
+    }
+
+    void finalize() {
+        dec_range_ref(m_nodes.begin(), m_nodes.end());
+        m_nodes.finalize();
+    }
+
+    void resize(unsigned sz) {
+        if (sz < m_nodes.size())
+            dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
+        m_nodes.resize(sz);
+    }
+
+    void resize(unsigned sz, elem_t d) {
+        if (sz < m_nodes.size()) {
+            dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
+            m_nodes.shrink(sz); 
+        }
+        else {
+            for (unsigned i = m_nodes.size(); i < sz; i++)
+                push_back(d);
+        }
+    }
+
+    void reserve(unsigned sz) {
+        if (sz <= m_nodes.size())
+            return;
+        m_nodes.resize(sz);
+    }
+
+    void shrink(unsigned sz) {
+        SASSERT(sz <= m_nodes.size());
+        dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
+        m_nodes.shrink(sz);
+    }
+
+    ref_pair_vector_core& push_back(elem_t n) {
+        inc_ref(n);
+        m_nodes.push_back(n);
+        return *this;
+    }
+
+    ref_pair_vector_core& push_back(T * a, T* b) {
+        return push_back(std::make_pair(a, b));
+    }
+
+    template <typename M>
+    ref_pair_vector_core& push_back(obj_ref<T,M> && n) {
+        m_nodes.push_back(n.get());
+        n.steal();
+        return *this;
+    }
+
+    void pop_back() {
+        SASSERT(!m_nodes.empty());
+        auto n = m_nodes.back();
+        m_nodes.pop_back();
+        dec_ref(n);
+    }
+
+    elem_t const& back() const { return m_nodes.back(); }
+
+    unsigned size() const { return m_nodes.size(); }
+
+    bool empty() const { return m_nodes.empty(); }
+
+    elem_t const& get(unsigned idx) const { return m_nodes[idx]; }
+
+    elem_t const * c_ptr() const { return m_nodes.begin(); }
+    
+    typedef elem_t const* iterator;
+
+    iterator begin() const { return m_nodes.begin(); }
+    iterator end() const { return begin() + size(); }
+    
+    elem_t operator[](unsigned idx) const {
+        return m_nodes[idx];
+    }
+
+    void append(ref_pair_vector_core const & other) {
+        for (unsigned i = 0; i < other.size(); ++i)
+            push_back(other[i]);
+    }
+
+    void swap(unsigned idx1, unsigned idx2) {
+        std::swap(m_nodes[idx1], m_nodes[idx2]);
+    }
+
+    void reverse() {
+        unsigned sz = size();
+        for (unsigned i = 0; i < sz/2; ++i) {
+            std::swap(m_nodes[i], m_nodes[sz-i-1]);
+        }
+    }
+};
+
+
+
+/**
+   \brief Vector of smart pointers.
+   TManager must provide the functions:
+   - void dec_ref(T * obj)
+   - void inc_ref(T * obj)
+*/
+template<typename T, typename TManager>
+class ref_pair_vector : public ref_pair_vector_core<T, ref_manager_wrapper<T, TManager> > {
+    typedef ref_pair_vector_core<T, ref_manager_wrapper<T, TManager> > super;
+
+public:
+    typedef std::pair<T*,T*> elem_t;
+
+    ref_pair_vector(TManager & m):
+        super(ref_manager_wrapper<T, TManager>(m)) {
+    }
+    
+    ref_pair_vector(ref_pair_vector const & other): 
+        super(ref_manager_wrapper<T, TManager>(other.m_manager)) {
+        this->append(other);
+    }
+
+    ref_pair_vector(ref_pair_vector && other) : super(std::move(other)) {}
+
+    ref_pair_vector(TManager & m, unsigned sz, elem_t const * data):
+        super(ref_manager_wrapper<T, TManager>(m)) {
+        this->append(sz, data);
+    }
+    
+    TManager & get_manager() const {
+        return this->m_manager;
+    }
+    
+    TManager & m() const { 
+        return get_manager();
+    }
+
+    void swap(ref_pair_vector & other) {
+        SASSERT(&(this->m_manager) == &(other.m_manager));
+        this->m_nodes.swap(other.m_nodes);
+    }
+    
+    class element_ref {
+        elem_t &       m_ref;
+        TManager &  m_manager;
+    public:
+        element_ref(elem_t & ref, TManager & m):
+            m_ref(ref),
+            m_manager(m) {
+        }
+
+        element_ref & operator=(elem_t n) {
+            m_manager.inc_ref(n.first);
+            m_manager.inc_ref(n.second);
+            m_manager.dec_ref(m_ref.first);
+            m_manager.dec_ref(m_ref.second);
+            m_ref = n;
+            return *this;
+        }
+
+        element_ref & operator=(element_ref& n) {
+            *this = n.get();
+            return *this;
+        }
+
+        template <typename W, typename M>
+        element_ref & operator=(obj_ref<W,M> && n) {
+            m_manager.dec_ref(m_ref);
+            m_ref = n.steal();
+            return *this;
+        }
+
+        elem_t get() const {
+            return m_ref;
+        }
+
+        elem_t operator->() const { 
+            return m_ref; 
+        }
+        
+        T const & operator*() const {
+            SASSERT(m_ref);
+            return *m_ref;
+        }
+        
+        bool operator==(elem_t n) const {
+            return m_ref == n;
+        }
+    };
+
+    elem_t operator[](unsigned idx) const { return super::operator[](idx); }
+
+    element_ref operator[](unsigned idx) {
+        return element_ref(this->m_nodes[idx], this->m_manager);
+    }
+
+    void set(unsigned idx, elem_t n) { super::set(idx, n); }
+    
+    // prevent abuse:
+    ref_pair_vector & operator=(ref_pair_vector const & other) = delete;
+
+    bool operator==(ref_pair_vector const& other) const {
+        if (other.size() != this->size()) return false;
+        for (unsigned i = this->size(); i-- > 0; ) {
+            if (other[i] != (*this)[i]) return false;
+        }
+        return true;
+    }
+
+    bool operator!=(ref_pair_vector const& other) const {
+        return !(*this == other);
+    }
+
+
+};
+
+
+
diff --git a/src/util/scoped_vector.h b/src/util/scoped_vector.h
index 5935ab6fa..aa64474d3 100644
--- a/src/util/scoped_vector.h
+++ b/src/util/scoped_vector.h
@@ -135,7 +135,8 @@ public:
 
     void erase_and_swap(unsigned i) {
         if (i + 1 < size()) {
-            set(i, m_elems[m_index[size()-1]]);
+            auto n = m_elems[m_index[size() - 1]];
+            set(i, n);
         }
         pop_back();
     }