diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 09e4bd3a9..9a9b17500 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -87,6 +87,10 @@ struct
     (z3obj_sno res ctx no) ;
     (z3obj_create res) ;
     res               
+ 
+   let ignore2 a b c = ignore a; ignore b
+   let ignore3 a b c = ignore a; ignore2 b c
+
 end
 
 open Internal
@@ -833,6 +837,22 @@ end = struct
       let o = Z3native.mk_app (context_gno ctx) (AST.ptr_of_ast fa) (List.length args) (expr_lton args) in
       expr_of_ptr ctx o
 
+   let apply_un ctx f t = 
+       let r = expr_of_ptr ctx (f (context_gno ctx) (gno t)) in
+       ignore t;
+       r
+
+   let apply_bin ctx f t1 t2 = 
+       let r = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) in
+       ignore2 t1 t2;
+       r
+
+   let apply_ter ctx f t1 t2 t3 = 
+       let r = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) in
+       ignore3 t1 t2 t3;
+       r
+
+
   let simplify ( x : expr ) ( p : Params.params option ) = match p with 
     | None -> expr_of_ptr (Expr.gc x) (Z3native.simplify (gnc x) (gno x))
     | Some pp -> expr_of_ptr (Expr.gc x) (Z3native.simplify_ex (gnc x) (gno x) (z3obj_gno pp))
@@ -854,13 +874,17 @@ end = struct
     if ((AST.is_app (ast_of_expr x)) && (List.length args <> (get_num_args x))) then
       raise (Z3native.Exception "Number of arguments does not match")
     else
-      expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args))
+      let r = expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) in
+      ignore2 x args;
+      r
 
   let substitute ( x : expr ) from to_ = 
     if (List.length from) <> (List.length to_) then
       raise (Z3native.Exception "Argument sizes do not match")
     else
-      expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_))
+      let r = expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) in
+      ignore3 from to_ x;
+      r 
      
   let substitute_one ( x : expr ) from to_ =
     substitute ( x : expr ) [ from ] [ to_ ]
@@ -872,7 +896,9 @@ end = struct
     if (Expr.gc x) == to_ctx then
       x
     else
-      expr_of_ptr to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx))
+      let r = expr_of_ptr to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx)) in
+      ignore2 x to_ctx;
+      r
 
   let to_string ( x : expr ) = Z3native.ast_to_string (gnc x) (gno x)
 
@@ -933,34 +959,39 @@ struct
   let mk_val ( ctx : context ) ( value : bool ) =
     if value then mk_true ctx else mk_false ctx
       
-  let mk_not ( ctx : context ) ( a : expr ) =
-    expr_of_ptr ctx (Z3native.mk_not (context_gno ctx) (gno a))
+  let mk_not ( ctx : context ) ( a : expr ) = apply_un ctx Z3native.mk_not a
 
-  let mk_ite ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_ite (context_gno ctx) (gno t1) (gno t2) (gno t3))
+  let mk_ite ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) = 
+    apply_ter ctx Z3native.mk_ite t1 t2 t3
       
   let mk_iff ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_iff (context_gno ctx) (gno t1) (gno t2))
+    apply_bin ctx Z3native.mk_iff t1 t2
 
   let mk_implies ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_implies (context_gno ctx) (gno t1) (gno t2))
+    apply_bin ctx Z3native.mk_implies t1 t2
 
   let mk_xor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_xor (context_gno ctx) (gno t1) (gno t2))
+    apply_bin ctx Z3native.mk_xor t1 t2
 
   let mk_and ( ctx : context ) ( args : expr list ) =
     let f x = (Expr.gno (x)) in
-    expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (List.length args) (Array.of_list (List.map f args)))
+    let r = expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (List.length args) (Array.of_list (List.map f args))) in
+    ignore args;
+    r
 
   let mk_or ( ctx : context ) ( args : expr list ) =
     let f x = (Expr.gno (x)) in
-    expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (List.length args) (Array.of_list(List.map f args)))
+    let r = expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (List.length args) (Array.of_list(List.map f args))) in
+    ignore args;
+    r
 
   let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) =
-    expr_of_ptr ctx (Z3native.mk_eq (context_gno ctx) (Expr.gno x) (Expr.gno y))
+    apply_bin ctx Z3native.mk_eq x y
 
   let mk_distinct ( ctx : context ) ( args : expr list ) =
-    expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args))
+    let r = expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args)) in
+    ignore args;
+    r
 
   let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value (gnc x) (gno x))
 
@@ -1066,10 +1097,12 @@ struct
     mk_list f n
       
   let get_body ( x : quantifier ) =
-    expr_of_ptr (gc x) (Z3native.get_quantifier_body (gnc x) (gno x))  
+    apply_un (gc x) Z3native.get_quantifier_body x
 
   let mk_bound ( ctx : context ) ( index : int ) ( ty : Sort.sort ) =
-    expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty))
+    let r = expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty)) in
+    ignore ty;
+    r
 
   let mk_pattern ( ctx : context ) ( terms : expr list ) =
     if (List.length terms) == 0 then
@@ -1194,23 +1227,27 @@ struct
     mk_const ctx (Symbol.mk_string ctx name) domain range
       
   let mk_select ( ctx : context ) ( a : expr ) ( i : expr ) =
-    expr_of_ptr ctx (Z3native.mk_select (context_gno ctx) (Expr.gno a) (Expr.gno i))      
+    apply_bin ctx Z3native.mk_select a i
 
   let mk_store ( ctx : context ) ( a : expr ) ( i : expr ) ( v : expr ) =
-    expr_of_ptr ctx (Z3native.mk_store (context_gno ctx) (Expr.gno a) (Expr.gno i) (Expr.gno v))
+    apply_ter ctx Z3native.mk_store a i v
 
   let mk_const_array ( ctx : context ) ( domain : Sort.sort ) ( v : expr ) =
-    expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v))
+    let r = expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v)) in
+    ignore2 domain v;
+    r
 
   let mk_map ( ctx : context ) ( f : func_decl ) ( args : expr list ) =
     let m x = (Expr.gno x) in    
-    expr_of_ptr ctx (Z3native.mk_map (context_gno ctx) (FuncDecl.gno f) (List.length args) (Array.of_list (List.map m args)))
+    let r = expr_of_ptr ctx (Z3native.mk_map (context_gno ctx) (FuncDecl.gno f) (List.length args) (Array.of_list (List.map m args))) in
+    ignore2 f args;
+    r
 
   let mk_term_array  ( ctx : context ) ( arg : expr ) =
-    expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (Expr.gno arg))
+    apply_un ctx Z3native.mk_array_default arg
 
   let mk_array_ext ( ctx : context) ( arg1 : expr ) ( arg2 : expr ) =
-     expr_of_ptr ctx (Z3native.mk_array_ext (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2))
+    apply_bin ctx Z3native.mk_array_ext arg1 arg2
 end
 
 
@@ -1233,13 +1270,15 @@ struct
     expr_of_ptr ctx (Z3native.mk_full_set (context_gno ctx) (Sort.gno domain))
 
   let mk_set_add  ( ctx : context ) ( set : expr ) ( element : expr ) =
-    expr_of_ptr ctx (Z3native.mk_set_add (context_gno ctx) (Expr.gno set) (Expr.gno element))
+    apply_bin ctx Z3native.mk_set_add set element
       
   let mk_del  ( ctx : context ) ( set : expr ) ( element : expr ) =
-    expr_of_ptr ctx (Z3native.mk_set_del (context_gno ctx) (Expr.gno set) (Expr.gno element))
+    apply_bin Z3native.mk_set_del set element
       
   let mk_union  ( ctx : context ) ( args : expr list ) =
-    expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args))
+    let r = expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args)) in
+    ignore r;
+    r
       
   let mk_intersection  ( ctx : context ) ( args : expr list ) =
     expr_of_ptr ctx (Z3native.mk_set_intersect (context_gno ctx) (List.length args) (expr_lton args))
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index ea5bec231..5b5ed1c55 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -42,7 +42,7 @@ zstring::zstring(unsigned num_bits, bool const* ch) {
     m_encoding = (num_bits == 8)?ascii:unicode;
     unsigned n = 0;    
     for (unsigned i = 0; i < num_bits; ++i) {
-        n |= (((unsigned)ch[i]) << num_bits);
+        n |= (((unsigned)ch[i]) << i);
     }
     m_buffer.push_back(n);
 }
@@ -81,12 +81,23 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
     return result;
 }
 
+static char* esc_table[32] = { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N",
+                               "^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"};
+ 
 std::string zstring::encode() const {
-    // TBD apply encodings.
     SASSERT(m_encoding == ascii);
     std::ostringstream strm;
     for (unsigned i = 0; i < m_buffer.size(); ++i) {
-        strm << (char)(m_buffer[i]);
+        unsigned char ch = m_buffer[i];
+        if (0 <= ch && ch < 32) {
+            strm << esc_table[ch];
+        }
+        else if (ch == 127) {
+            strm << "^?";
+        }
+        else {
+            strm << (char)(ch);
+        }
     }
     return strm.str();
 }
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 98d982b7a..16cf18d2e 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -90,7 +90,9 @@ namespace smt {
                 sort * s      = m_manager.get_sort(r->get_owner());
                 model_value_proc * proc = 0;
                 if (m_manager.is_bool(s)) {
-                    SASSERT(m_context->get_assignment(r) == l_true || m_context->get_assignment(r) == l_false);
+                    CTRACE("func_interp_bug", m_context->get_assignment(r) == l_undef, 
+                           tout << mk_pp(r->get_owner(), m_manager) << "\n";);
+                    SASSERT(m_context->get_assignment(r) != l_undef);
                     if (m_context->get_assignment(r) == l_true)
                         proc = alloc(expr_wrapper_proc, m_manager.mk_true());
                     else
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 62e4f4338..79779d088 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -132,6 +132,7 @@ theory_seq::theory_seq(ast_manager& m):
     m_incomplete(false), 
     m_has_length(false),
     m_model_completion(false),
+    m_mg(0),
     m_rewrite(m), 
     m_util(m),
     m_autil(m),
@@ -181,7 +182,7 @@ final_check_status theory_seq::final_check_eh() {
     }
     if (!check_length_coherence_tbd()) {
         TRACE("seq", tout << "check_length_coherence\n";);
-        return FC_GIVEUP;
+        return FC_CONTINUE;
     }
     if (is_solved()) {
         TRACE("seq", tout << "is_solved\n";);
@@ -400,15 +401,15 @@ void theory_seq::propagate_lit(enode_pair_dependency* dep, literal lit) {
     ctx.assign(lit, js);
 }
 
-void theory_seq::set_conflict(enode_pair_dependency* dep) {
+void theory_seq::set_conflict(enode_pair_dependency* dep, literal_vector const& lits) {
     context& ctx = get_context();
     vector<enode_pair, false> _eqs;
     m_dm.linearize(dep, _eqs);
-    TRACE("seq", display_deps(tout, dep);); 
+    TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); display_deps(tout, dep); ;); 
     ctx.set_conflict(
         ctx.mk_justification(
             ext_theory_conflict_justification(
-                get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), 0, 0)));
+                get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), _eqs.size(), _eqs.c_ptr(), 0, 0)));
 }
 
 void theory_seq::propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2) {
@@ -524,6 +525,10 @@ bool theory_seq::is_right_select(expr* a, expr*& b) {
         to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_right_sym && (b = to_app(a)->get_arg(0), true);
 }
 
+bool theory_seq::is_head_elem(expr* e) const {
+    return m_util.is_skolem(e) && to_app(e)->get_decl()->get_parameter(0).get_symbol() == symbol("seq.head.elem");
+}
+
 void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) {
     context& ctx = get_context();
     m_rep.update(l, r, deps);
@@ -583,17 +588,17 @@ bool theory_seq::solve_ne(unsigned idx) {
     TRACE("seq", display_disequation(tout, n););
 
     SASSERT(!n.is_solved());
+    unsigned num_undef_lits = 0;
     for (unsigned i = 0; i < n.m_lits.size(); ++i) {
         switch (ctx.get_assignment(n.m_lits[i])) {
-        case l_true:
-            erase_lit(idx, i);
-            --i;
-            break;
         case l_false:
             // mark as solved in 
             mark_solved(idx);
             return false;
+        case l_true:
+            break;            
         case l_undef:
+            ++num_undef_lits;
             break;
         }
     }
@@ -630,29 +635,25 @@ bool theory_seq::solve_ne(unsigned idx) {
                 }
                 else {
                     literal lit(mk_eq(nl, nr, false));
-                    m_trail_stack.push(push_lit(*this, idx, ~lit));
+                    m_trail_stack.push(push_lit(*this, idx, lit));
                     ctx.mark_as_relevant(lit);
                 }
             }                
             m_trail_stack.push(push_dep(*this, idx, deps));
             erase_index(idx, i);
             --i;
+            change = true;
         }
     }
-    if (n.m_lits.empty() && n.m_lhs.empty()) {
-        set_conflict(n.m_dep);
+    if (num_undef_lits == 0 && n.m_lhs.empty()) {
+        literal_vector lits(n.m_lits);
+        lits.push_back(~mk_eq(n.m_l, n.m_r, false));
+        set_conflict(n.m_dep, lits);
         return true;
     }
     return change;
 }
 
-void theory_seq::erase_lit(unsigned idx, unsigned i) {
-    ne const& n = m_nqs[idx];
-    if (n.m_lits.size() < i + 1) {
-        m_trail_stack.push(set_lit(*this, idx, i, n.m_lits.back()));        
-    }
-    m_trail_stack.push(pop_lit(*this, idx));
-}
 
 void theory_seq::mark_solved(unsigned idx) {
     m_trail_stack.push(solved_ne(*this, idx));
@@ -810,8 +811,12 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
     enode_pair_dependency* deps = 0;
     expr_ref e(n->get_owner(), m);
     flet<bool> _model_completion(m_model_completion, true);
+    m_rep.reset_cache();
+    m_mg = &mg;
     e = canonize(e, deps);
+    m_mg = 0;
     SASSERT(is_app(e));
+    TRACE("seq", tout << mk_pp(n->get_owner(), m) << " -> " << e << "\n";);
     m_factory->add_trail(e);
     return alloc(expr_wrapper_proc, to_app(e));
 }
@@ -852,15 +857,17 @@ expr_ref theory_seq::canonize(expr* e, enode_pair_dependency*& eqs) {
     return result;
 }
 
-expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) {
+expr_ref theory_seq::expand(expr* e0, enode_pair_dependency*& eqs) {
+    expr_ref result(m);
     enode_pair_dependency* deps = 0;
     expr_dep ed;
-    if (m_rep.find_cache(e, ed)) {
+    if (m_rep.find_cache(e0, ed)) {
         eqs = m_dm.mk_join(eqs, ed.second);
-        return expr_ref(ed.first, m);
+        result = ed.first;
+        TRACE("seq", tout << mk_pp(e0, m) << " |-> " << result << " "; display_deps(tout, eqs););
+        return result;
     }
-    e = m_rep.find(e, deps);
-    expr_ref result(m);
+    expr* e = m_rep.find(e0, deps);
     expr* e1, *e2;
     if (m_util.str.is_concat(e, e1, e2)) {
         result = m_util.str.mk_concat(expand(e1, deps), expand(e2, deps));
@@ -889,15 +896,43 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) {
             result = e;
         }
     }
+    else if (m_model_completion && m_util.str.is_unit(e, e1)) {
+        result = expand(e1, deps);
+        bv_util bv(m);
+        rational val;
+        unsigned sz;
+        if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) {
+            svector<bool> val_as_bits;
+            for (unsigned i = 0; i < sz; ++i) {
+                val_as_bits.push_back(!val.is_even());
+                val = div(val, rational(2));
+            }
+            result = m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr()));
+        }
+        else {
+            result = m_util.str.mk_unit(result);
+        }
+    }
+    else if (m_model_completion && is_head_elem(e)) {
+        enode* n = get_context().get_enode(e)->get_root();
+        result = n->get_owner();
+        if (!m.is_model_value(result)) {
+            result = m_mg->get_some_value(m.get_sort(result));
+        }
+        m_rep.update(e, result, 0);        
+        TRACE("seq", tout << mk_pp(e, m) << " |-> " << result << "\n";);
+    }
     else {
         result = e;
     }
-    if (result == e) {
+    if (result == e0) {
         deps = 0;
     }
     expr_dep edr(result, deps);
-    m_rep.add_cache(e, edr);
+    m_rep.add_cache(e0, edr);
     eqs = m_dm.mk_join(eqs, deps);
+    TRACE("seq", tout << mk_pp(e0, m) << " |--> " << result << "\n";
+          display_deps(tout, eqs););
     return result;
 }
 
@@ -1116,8 +1151,9 @@ void theory_seq::add_length_concat_axiom(expr* n) {
     expr_ref len(m_util.str.mk_length(n), m);
     expr_ref _a(m_util.str.mk_length(a), m);
     expr_ref _b(m_util.str.mk_length(b), m);
-    expr_ref a_p_b(m_autil.mk_add(_a, _b), m);
-    add_axiom(mk_eq(len, a_p_b, false));
+    expr_ref ab(m_autil.mk_add(_a, _b), m);
+    m_rewrite(ab);
+    add_axiom(mk_eq(ab, len, false));
 }
 
 /*
@@ -1144,8 +1180,10 @@ void theory_seq::add_length_axiom(expr* n) {
     }
 }
 
-expr* theory_seq::mk_sub(expr* a, expr* b) {
-    return m_autil.mk_add(a, m_autil.mk_mul(m_autil.mk_int(-1), b));
+expr_ref theory_seq::mk_sub(expr* a, expr* b) {
+    expr_ref result(m_autil.mk_sub(a, b), m);
+    m_rewrite(result);
+    return result;
 }
 
 enode* theory_seq::ensure_enode(expr* e) {
@@ -1325,7 +1363,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     enode* n2 = get_enode(v2);
     expr_ref e1(n1->get_owner(), m);
     expr_ref e2(n2->get_owner(), m);
-    m_nqs.push_back(ne(e1, e2, m_dm.mk_leaf(enode_pair(n1, n2))));
+    m_nqs.push_back(ne(e1, e2));
     m_exclude.update(e1, e2);
 }
 
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 59ae5095a..21aabb599 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -70,6 +70,7 @@ namespace smt {
             bool  find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); }
             expr* find(expr* e, enode_pair_dependency*& d);
             void  cache(expr* e, expr* r, enode_pair_dependency* d);
+            void reset_cache() { m_cache.reset(); }
             void push_scope() { m_limit.push_back(m_updates.size()); }
             void pop_scope(unsigned num_scopes);
             void display(std::ostream& out) const;
@@ -108,19 +109,22 @@ namespace smt {
         // asserted or derived disqequality with dependencies
         struct ne {
             bool                   m_solved;
+            expr_ref               m_l, m_r;
             expr_ref_vector        m_lhs;
             expr_ref_vector        m_rhs;
             literal_vector         m_lits;
             enode_pair_dependency* m_dep;
-            ne(expr_ref& l, expr_ref& r, enode_pair_dependency* d):
-                m_solved(false), m_lhs(l.get_manager()), m_rhs(r.get_manager()), m_dep(d) {
+            ne(expr_ref& l, expr_ref& r):
+                m_solved(false), m_l(l), m_r(r), m_lhs(l.get_manager()), m_rhs(r.get_manager()), m_dep(0) {
                 m_lhs.push_back(l);
                 m_rhs.push_back(r);
             }
             ne(ne const& other): 
-                m_solved(other.m_solved), m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
+                m_solved(other.m_solved), 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) {}
             ne& operator=(ne const& other) { 
                 m_solved = other.m_solved;
+                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_lits.reset(); m_lits.append(other.m_lits); 
@@ -158,7 +162,6 @@ namespace smt {
             }
             virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits[m_i] = m_lit; }            
         };
-        void erase_lit(unsigned idx, unsigned i);
 
         class solved_ne : public trail<theory_seq> {
             unsigned m_idx;
@@ -255,6 +258,7 @@ namespace smt {
         bool            m_incomplete;            // is the solver (clearly) incomplete for the fragment.
         bool            m_has_length;            // is length applied
         bool            m_model_completion;      // during model construction, invent values in canonizer
+        model_generator* m_mg;
         th_rewriter     m_rewrite;
         seq_util        m_util;
         arith_util      m_autil;
@@ -313,7 +317,7 @@ namespace smt {
         void propagate_lit(enode_pair_dependency* dep, literal lit);
         void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2);
         void propagate_eq(bool_var v, expr* e1, expr* e2);
-        void set_conflict(enode_pair_dependency* dep);
+        void set_conflict(enode_pair_dependency* dep, literal_vector const& lits = literal_vector());
 
         bool find_branch_candidate(expr* l, expr_ref_vector const& rs);
         bool assume_equality(expr* l, expr* r);
@@ -324,6 +328,7 @@ namespace smt {
         void add_solution(expr* l, expr* r, enode_pair_dependency* dep);
         bool is_left_select(expr* a, expr*& b);
         bool is_right_select(expr* a, expr*& b);
+        bool is_head_elem(expr* a) const;
         expr_ref canonize(expr* e, enode_pair_dependency*& eqs);
         expr_ref expand(expr* e, enode_pair_dependency*& eqs);
         void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b);
@@ -345,7 +350,7 @@ namespace smt {
         void add_at_axiom(expr* n);
         literal mk_literal(expr* n);
         void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
-        expr* mk_sub(expr* a, expr* b);
+        expr_ref mk_sub(expr* a, expr* b);
         enode* ensure_enode(expr* a);
 
         expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0);