diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 1231369c7..3ee8675d8 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1001,7 +1001,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
         }
         if (l < s2.length()) {
             rs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l)));
-        }
+        }        
         change = true;
     }
 
@@ -1023,27 +1023,17 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
     }
     else if (!change) {
         // skip
+        SASSERT(lhs.empty());
     }
     else {
         // could solve if either side is fixed size.
         SASSERT(szl > 0 && szr > 0);
-        if (head1 > 0) {
-            for (unsigned i = 0; i < szl; ++i) {
-                ls[i] = ls[i + head1];
-            }			
-        }
-        ls.shrink(szl);
-        if (head2 > 0) {
-            for (unsigned i = 0; i < szr; ++i) {
-                rs[i] = rs[i + head2];
-            }
-        }
-        rs.shrink(szr);        
-        lhs.push_back(m_util.str.mk_concat(ls.size(), ls.c_ptr()));
-        rhs.push_back(m_util.str.mk_concat(rs.size(), rs.c_ptr()));
+        lhs.push_back(m_util.str.mk_concat(szl, ls.c_ptr() + head1));
+        rhs.push_back(m_util.str.mk_concat(szr, rs.c_ptr() + head2));
         ls.reset();
         rs.reset();
     }
+    SASSERT(lhs.empty() || ls.empty());
     return true;
 }
 
@@ -1054,16 +1044,9 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
     m_util.str.get_concat(r, m_rhs);
     if (reduce_eq(m_lhs, m_rhs, lhs, rhs)) {
         SASSERT(lhs.size() == rhs.size());
-        if (!m_lhs.empty()) {
-            SASSERT(!m_rhs.empty());
-            lhs.push_back(m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr()));
-            rhs.push_back(m_util.str.mk_concat(m_rhs.size(), m_rhs.c_ptr()));            
-        }
-        for (unsigned i = 0; i < lhs.size(); ++i) {
-            SASSERT(is_well_sorted(m(), lhs[i].get()));
-            SASSERT(is_well_sorted(m(), rhs[i].get()));
-            SASSERT(m().get_sort(lhs[i].get()) == m().get_sort(rhs[i].get()));
-            TRACE("seq", tout << mk_pp(lhs[i].get(), m()) << " = " << mk_pp(rhs[i].get(), m()) << "\n";);
+        if (lhs.empty()) {
+            lhs.push_back(l);
+            rhs.push_back(r);
         }
         return true;
     }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 7aa434661..e3ede010c 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -166,6 +166,8 @@ theory_seq::theory_seq(ast_manager& m):
     m_autil(m),
     m_trail_stack(*this),
     m_atoms_qhead(0),
+    m_ls(m), m_rs(m),
+    m_lhs(m), m_rhs(m),
     m_new_solution(false),
     m_new_propagation(false) {    
     m_prefix = "seq.prefix.suffix";
@@ -874,17 +876,21 @@ void theory_seq::solve_ne(unsigned idx) {
         }
     }
     for (unsigned i = 0; i < n.m_lhs.size(); ++i) {
-        expr_ref_vector lhs(m), rhs(m);
+        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 = 0;
         expr* l = n.m_lhs[i];
         expr* r = n.m_rhs[i];
-        expr_ref lh = canonize(l, deps);
-        expr_ref rh = canonize(r, deps);
-        if (!rw.reduce_eq(lh, rh, lhs, rhs)) {
+        canonize(l, ls, deps);
+        canonize(r, rs, deps);
+        if (!rw.reduce_eq(ls, rs, lhs, rhs)) {
             mark_solved(idx);
             return;
         }
-        else if (unchanged(l, lhs, r, rhs) ) {
+        else if (lhs.empty() || (lhs.size() == 1 && lhs[0].get() == l)) {
             // continue
         }
         else {
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 511c6917c..cd8d67cd1 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -318,6 +318,7 @@ namespace smt {
         symbol           m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
         symbol           m_extract_prefix, m_at_left, m_at_right;
         ptr_vector<expr> m_todo;
+        expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
 
         // maintain automata with regular expressions.
         scoped_ptr_vector<eautomaton>  m_automata;