diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index cbccfeb5e..1b1d6c450 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -383,7 +383,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     zstring s;
     rational pos, len;
     if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
-        pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) {
+        pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() + len.get_unsigned() <= s.length()) {
         unsigned _pos = pos.get_unsigned();
         unsigned _len = len.get_unsigned();
         result = m_util.str.mk_string(s.extract(_pos, _len));
@@ -538,34 +538,40 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
             }
         }        
     }
-    if (a1 != b1) {
-        return BR_FAILED;
-    }
     m_util.str.get_concat(a, as);
     m_util.str.get_concat(b, bs);
     unsigned i = 0;
     bool all_values = true;    
+    expr_ref_vector eqs(m());
     for (; i < as.size() && i < bs.size(); ++i) {
-        all_values &= m().is_value(as[i].get()) && m().is_value(bs[i].get());
-        if (as[i].get() != bs[i].get()) {
-            if (all_values) {
-                result = m().mk_false();
-                return BR_DONE;
-            }
-            break;
+        expr* a = as[i].get(), *b = bs[i].get();
+        if (a == b) {
+            continue;
         }
-    };
+        all_values &= m().is_value(a) && m().is_value(b);
+        if (all_values) {
+            result = m().mk_false();
+            return BR_DONE;
+        }
+        if (m_util.str.is_unit(a) && m_util.str.is_unit(b)) {
+            eqs.push_back(m().mk_eq(a, b));
+            continue;
+        }
+        break;
+    }
     if (i == as.size()) {
-        result = m().mk_true();
-        return BR_DONE;
+        result = mk_and(eqs);
+        if (m().is_true(result)) {
+            return BR_DONE;
+        }
+        return BR_REWRITE3;
     }
     SASSERT(i < as.size());
     if (i == bs.size()) {
-        expr_ref_vector es(m());
         for (unsigned j = i; j < as.size(); ++j) {
-            es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
+            eqs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
         }
-        result = mk_and(es);
+        result = mk_and(eqs);
         return BR_REWRITE3;
     }
     if (i > 0) {
@@ -575,8 +581,9 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
         result = m_util.str.mk_prefix(a, b);
         return BR_DONE;
     }
-    UNREACHABLE();
-    return BR_FAILED;
+    else {
+        return BR_FAILED;
+    }
 }
 
 br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
@@ -1221,19 +1228,19 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
             SASSERT(m().get_sort(ch) == m().get_sort(a));
             lhs.push_back(ch);
             rhs.push_back(a);
-            ls.pop_back();
+            ++head1;
             if (s.length() == 1) {
-                rs.pop_back();
+                ++head2;
             }
             else {
                 expr_ref s2(m_util.str.mk_string(s.extract(1, s.length()-1)), m());
-                rs[rs.size()-1] = s2;
+                rs[head2] = s2;
             }            
         }
         else {
             break;
         }
-        TRACE("seq", tout << "change front\n";);
+        TRACE("seq", tout << ls << " == " << rs << "\n";);
        
         change = true;
         lchange = true;
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index c137801ff..f15e83381 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -143,11 +143,15 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
         if (eq) {
             result.m_buffer.append(dst.m_buffer);
             found = true;
+            i += src.length() - 1;
         }
         else {
             result.m_buffer.push_back(m_buffer[i]);
         }
     }
+    for (unsigned i = length() - src.length() + 1; i < length(); ++i) {
+        result.m_buffer.push_back(m_buffer[i]);
+    }
     return result;
 }
 
@@ -554,7 +558,11 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
             parameter param(symbol(""));
             return mk_func_decl(OP_STRING_CONST, 1, &param, 0, 0, m_string);
         }
-        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+        else {
+            parameter param(rng.get());
+            func_decl_info info(m_family_id, k, 1, &param);
+            return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, info);
+        }
         
     case OP_SEQ_UNIT:
     case OP_RE_PLUS:
@@ -736,6 +744,19 @@ bool seq_decl_plugin::is_value(app* e) const {
          m_manager->is_value(e->get_arg(0)));
 }
 
+expr* seq_decl_plugin::get_some_value(sort* s) {
+    seq_util util(*m_manager);
+    if (util.is_seq(s)) {
+        return util.str.mk_empty(s);
+    }
+    sort* seq;
+    if (util.is_re(s, seq)) {
+        return util.re.mk_to_re(util.str.mk_empty(seq));
+    }
+    UNREACHABLE();
+    return 0;
+}
+
 app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
     SASSERT(range);
     parameter param(name);
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 29ec98b07..a83878b0e 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -177,10 +177,13 @@ public:
 
     virtual bool is_unique_value(app * e) const { return is_value(e); }
 
+    virtual expr * get_some_value(sort * s);
+
     bool is_char(ast* a) const { return a == m_char; }
 
     app* mk_string(symbol const& s);  
     app* mk_string(zstring const& s);  
+
 };
 
 class seq_util {
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index bc39577db..eb18c5262 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1638,6 +1638,7 @@ void cmd_context::validate_model() {
                 catch (contains_array_op_proc::found) {
                     continue;
                 }
+                TRACE("model_validate", model_smt2_pp(tout, *this, *(md.get()), 0););
                 throw cmd_exception("an invalid model was generated");
             }
         }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 71f1b03ea..f4e6d1d57 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -70,7 +70,6 @@ expr* theory_seq::solution_map::find(expr* e, dependency*& d) {
     expr* result = e;
     while (m_map.find(result, value)) {
         d = m_dm.mk_join(d, value.second);
-        TRACE("seq", tout << mk_pp(result, m) << " -> " << mk_pp(value.first, m) << "\n";);
         SASSERT(result != value.first);
         SASSERT(e != value.first);
         result = value.first;
@@ -195,7 +194,7 @@ theory_seq::~theory_seq() {
 
 
 final_check_status theory_seq::final_check_eh() {
-    TRACE("seq", display(tout););
+    TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
     if (simplify_and_solve_eqs()) {
         ++m_stats.m_solve_eqs;
         TRACE("seq", tout << ">>solve_eqs\n";);
@@ -422,12 +421,12 @@ bool theory_seq::propagate_length_coherence(expr* e) {
     tail = mk_concat(elems.size(), elems.c_ptr());
     // len(e) >= low => e = tail;
     literal low(mk_literal(m_autil.mk_ge(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true))));
-    add_axiom(~low, mk_eq(e, tail, false));
+    add_axiom(~low, mk_seq_eq(e, tail));
     if (upper_bound(e, hi)) {
         // len(e) <= hi => len(tail) <= hi - lo
         expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m);
         if (hi == lo) {
-            add_axiom(~mk_literal(high1), mk_eq(seq, emp, false));
+            add_axiom(~mk_literal(high1), mk_seq_eq(seq, emp));
         }
         else {
             expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m);
@@ -501,6 +500,11 @@ bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const {
         (idx = r.get_unsigned(), s = to_app(e)->get_arg(0), true);
 }
 
+bool theory_seq::is_eq(expr* e, expr*& a, expr*& b) const {
+    return is_skolem(symbol("seq.eq"), e) &&
+        (a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true);
+}
+
 
 expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
     sort* char_sort = 0;
@@ -608,15 +612,23 @@ bool theory_seq::check_extensionality() {
 
 bool theory_seq::is_solved() {
     if (!m_eqs.empty()) {
+        TRACE("seq", tout << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
         IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
         return false;
     }
     for (unsigned i = 0; i < m_automata.size(); ++i) {
         if (!m_automata[i]) {
+            TRACE("seq", tout  << "(seq.giveup regular expression did not compile to automaton)\n";);
             IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";);
             return false;
         }
     }
+    if (false && !m_nqs.empty()) {
+        TRACE("seq", display_disequation(tout << "(seq.giveup ", m_nqs[0]); tout << " is unsolved)\n";);
+        IF_VERBOSE(10, display_disequation(verbose_stream() << "(seq.giveup ", m_nqs[0]); verbose_stream() << " is unsolved)\n";);
+        return false;
+    }
+
     return true;
 }
 
@@ -737,11 +749,10 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
         }
     }
     TRACE("seq",
-          tout << ls << " = " << rs << " => \n";
+          if (!ls.empty() || !rs.empty()) tout << ls << " = " << rs << ";\n";
           for (unsigned i = 0; i < lhs.size(); ++i) {
-              tout << mk_pp(lhs[i].get(), m) << "\n = \n" << mk_pp(rhs[i].get(), m) << "; \n";
-          }
-          tout << "\n";);
+              tout << mk_pp(lhs[i].get(), m) << " = " << mk_pp(rhs[i].get(), m) << ";\n";
+          });
 
 
     return true;
@@ -844,7 +855,6 @@ bool theory_seq::solve_eqs(unsigned i) {
             change = true;
         }
     }
-    TRACE("seq", tout << "solve_eqs\n";);
     return change || ctx.inconsistent();
 }
 
@@ -1005,12 +1015,12 @@ bool theory_seq::solve_nqs(unsigned i) {
 bool theory_seq::solve_ne(unsigned idx) {
     context& ctx = get_context();
     ne const& n = m_nqs[idx];
-    TRACE("seq", display_disequation(tout, n););
 
     unsigned num_undef_lits = 0;
     for (unsigned i = 0; i < n.lits().size(); ++i) {
         switch (ctx.get_assignment(n.lits(i))) {
         case l_false:
+            TRACE("seq", display_disequation(tout << "has false literal\n", n););
             return true;
         case l_true:
             break;
@@ -1036,6 +1046,7 @@ bool theory_seq::solve_ne(unsigned idx) {
         change = canonize(n.rs(i), rs, deps) || change;
 
         if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, change)) {
+            TRACE("seq", display_disequation(tout << "reduces to false", n););
             return true;
         }
         else if (!change) {
@@ -1060,10 +1071,8 @@ bool theory_seq::solve_ne(unsigned idx) {
                 new_rs.push_back(rs);
             }
             TRACE("seq",
-                  for (unsigned j = 0; j < lhs.size(); ++j) {
-                      tout << mk_pp(lhs[j].get(), m) << " " << mk_pp(rhs[j].get(), m) << "\n";
-                  }
-                  tout << "\n";
+                  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) {
@@ -1096,6 +1105,9 @@ bool theory_seq::solve_ne(unsigned idx) {
             new_deps = m_dm.mk_join(deps, new_deps);
         }
     }
+
+    TRACE("seq", display_disequation(tout, n););
+
     if (!updated && num_undef_lits == 0) {
         return false;
     }
@@ -1162,7 +1174,7 @@ bool theory_seq::internalize_term(app* term) {
         mk_var(e);
         return true;
     }
-    TRACE("seq", tout << mk_pp(term, m) << "\n";);
+    TRACE("seq_verbose", tout << mk_pp(term, m) << "\n";);
     unsigned num_args = term->get_num_args();
     expr* arg;
     for (unsigned i = 0; i < num_args; i++) {
@@ -1333,146 +1345,106 @@ void theory_seq::init_model(model_generator & mg) {
 }
 
 
-class seq_value_proc : public model_value_proc {
-    theory_seq& th;
-    app* n;
+class theory_seq::seq_value_proc : public model_value_proc {
+    theory_seq&                     th;
+    sort*                           m_sort;
     svector<model_value_dependency> m_dependencies;
+    ptr_vector<expr>                m_strings;
+    svector<bool>                   m_source;
 public:
-    seq_value_proc(theory_seq& th, app* n): th(th), n(n) {
+    seq_value_proc(theory_seq& th, sort* s): th(th), m_sort(s) {
     }
     virtual ~seq_value_proc() {}
-    void add_dependency(enode* n) { m_dependencies.push_back(model_value_dependency(n)); }
+    void add_dependency(enode* n) { 
+        m_dependencies.push_back(model_value_dependency(n)); 
+        m_source.push_back(true);
+    }
+    void add_string(expr* n) {
+        m_strings.push_back(n);
+        m_source.push_back(false);
+    }
     virtual void get_dependencies(buffer<model_value_dependency> & result) {
         result.append(m_dependencies.size(), m_dependencies.c_ptr());
     }
     virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
         SASSERT(values.size() == m_dependencies.size());
-        if (values.empty()) {
-            return th.mk_value(n);
+        expr_ref_vector args(th.m);
+        unsigned j = 0, k = 0;
+        bool is_string = th.m_util.is_string(m_sort);
+        for (unsigned i = 0; i < m_source.size(); ++i) {
+            if (m_source[i] && is_string) {
+                bv_util bv(th.m);
+                rational val;
+                unsigned sz;
+                VERIFY(bv.is_numeral(values[j++], val, sz));
+                svector<bool> val_as_bits;
+                unsigned v = val.get_unsigned();
+                for (unsigned i = 0; i < sz; ++i) {
+                    val_as_bits.push_back(1 == v % 2);
+                    v = v / 2;
+                }
+                args.push_back(th.m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr())));
+            }
+            else if (m_source[i]) {
+                args.push_back(th.m_util.str.mk_unit(values[j++]));
+            }
+            else {
+                args.push_back(m_strings[k++]);
+            }
         }
-        return th.mk_value(mg.get_manager().mk_app(n->get_decl(), values.size(), values.c_ptr()));
+        expr_ref result = th.mk_concat(args, m_sort);
+        th.m_rewrite(result);
+        th.m_factory->add_trail(result);
+        return to_app(result);
     }
 };
 
 
 model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
-    context& ctx = get_context();
-    expr_ref e(m);
-    expr* e1;
-    ptr_vector<expr> concats;
-    get_concat(n->get_owner(), concats);
-    switch (concats.size()) {
-    case 0:
-        e = m_util.str.mk_empty(m.get_sort(n->get_owner()));
-        break;
-    case 1:
-        e = concats[0];
-        SASSERT(!m_util.str.is_concat(e));
-        break;
-    default:
-        e = m_rep.find(n->get_owner());
-        SASSERT(m_util.str.is_concat(e));
-        break;
-    }
-    seq_value_proc* sv = alloc(seq_value_proc, *this, to_app(e));
-    TRACE("seq", tout << mk_pp(n->get_owner(), m) << " ";
-          for (unsigned i = 0; i < concats.size(); ++i) {
-              tout << mk_pp(concats[i], m) << " ";
-          }
-          tout << "\n";
-          );
-
-    if (concats.size() > 1) {
+    if (m_util.is_seq(n->get_owner())) {
+        ptr_vector<expr> concats;
+        get_concat(n->get_owner(), concats);
+        context& ctx = get_context();
+        sort* srt = m.get_sort(n->get_owner());
+        seq_value_proc* sv = alloc(seq_value_proc, *this, srt);
+        
         for (unsigned i = 0; i < concats.size(); ++i) {
-            expr* e = concats[i];
-            if (!m_util.str.is_string(e)) {
-                sv->add_dependency(ctx.get_enode(e));
+            expr* c = concats[i], *c1;
+            if (m_util.str.is_unit(c, c1)) {
+                sv->add_dependency(ctx.get_enode(c1));
             }
-        }
-    }
-    else if (m_util.str.is_unit(e, e1)) {
-        sv->add_dependency(ctx.get_enode(e1));
-    }
-    return sv;
-}
-
-void theory_seq::get_concat(expr* e, ptr_vector<expr>& concats) {
-    expr* e1, *e2;
-    while (true) {
-        e = m_rep.find(e);
-        if (m_util.str.is_concat(e, e1, e2)) {
-            get_concat(e1, concats);
-            e = e2;
-            continue;
-        }
-        if (!m_util.str.is_empty(e)) {
-            concats.push_back(e);
-        }
-        return;
-    }
-}
-
-app* theory_seq::mk_value(app* e) {
-    expr* e1;
-    expr_ref result(e, m);
-    if (m_util.str.is_unit(e, e1)) {
-        dependency* deps = 0;
-        result = expand(e1, deps);
-        bv_util bv(m);
-        rational val;
-        unsigned sz;
-        if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) {
-            unsigned v = val.get_unsigned();
-            if (false && ((v < 7) || (14 <= v && v < 32) || v == 127)) {
-                // disabled: use escape characters.
-                result = m_util.str.mk_unit(result);
+            else if (m_util.str.is_string(c)) {
+                sv->add_string(c);
             }
             else {
-                svector<bool> val_as_bits;
-                for (unsigned i = 0; i < sz; ++i) {
-                    val_as_bits.push_back(1 == v % 2);
-                    v = v / 2;
-                }
-                result = m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr()));
+                sv->add_string(mk_value(to_app(c)));
             }
         }
-        else {
-            result = m_util.str.mk_unit(result);
-        }
+        return sv;
     }
-    else if (is_var(e)) {
+    else {
+        return alloc(expr_wrapper_proc, mk_value(n->get_owner()));
+    }
+}
+
+
+app* theory_seq::mk_value(app* e) {
+    expr_ref result(m);
+    result = m_rep.find(e);
+    if (is_var(result)) {
         SASSERT(m_factory);
         expr_ref val(m);
-        val = m_factory->get_some_value(m.get_sort(e));
+        val = m_factory->get_some_value(m.get_sort(result));
         if (val) {
             result = val;
         }
-        else {
-            result = e;
-        }
     }
-    else if (is_nth(e)) {
-        enode* n = get_context().get_enode(e)->get_root();
-        enode* n0 = n;
-        bool found_value = false;
-        do {
-            result = n->get_owner();
-            found_value = m.is_model_value(result);
-        }
-        while (n0 != n && !found_value);
-
-        if (!found_value) {
-            if (m_util.is_char(result)) {
-                result = m_util.str.mk_char('#');
-            }
-            else {
-                result = m_mg->get_some_value(m.get_sort(result));
-            }
-        }
+    else {
+        m_rewrite(result);
     }
-    m_rewrite(result);
     m_factory->add_trail(result);
     TRACE("seq", tout << mk_pp(e, m) << " -> " << result << "\n";);
+    m_rep.update(e, result, 0);
     return to_app(result);
 }
 
@@ -1639,19 +1611,19 @@ void theory_seq::deque_axiom(expr* n) {
 
 
 /*
-  encode that s is not a proper prefix of xs1
+  encode that s is not contained in of xs1
   where s1 is all of s, except the last element.
 
   lit or s = "" or s = s1*(unit c)
-  lit or s = "" or !prefix(s, x*s1)
+  lit or s = "" or !contains(x*s1, s)
 */
 void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
     expr_ref s1 = mk_first(s);
     expr_ref c  = mk_last(s);
     expr_ref s1c = mk_concat(s1, m_util.str.mk_unit(c));
     literal s_eq_emp = mk_eq_empty(s);
-    add_axiom(lit1, lit2, s_eq_emp, mk_eq(s, s1c, false));
-    add_axiom(lit1, lit2, s_eq_emp, ~mk_literal(m_util.str.mk_prefix(s, mk_concat(x, s1))));
+    add_axiom(s_eq_emp, mk_seq_eq(s, s1c));
+    add_axiom(lit1, lit2, s_eq_emp, ~mk_literal(m_util.str.mk_contains(mk_concat(x, s1), s)));
 }
 
 /*
@@ -1692,15 +1664,17 @@ void theory_seq::add_indexof_axiom(expr* i) {
 
 
     if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
-        expr_ref x  = mk_skolem(m_contains_left, t, s);
-        expr_ref y  = mk_skolem(m_contains_right, t, s);
+        expr_ref x  = mk_skolem(m_indexof_left, t, s);
+        expr_ref y  = mk_skolem(m_indexof_right, t, s);
         xsy         = mk_concat(x, s, y);
+        expr_ref lenx(m_util.str.mk_length(x), m);
         literal cnt = mk_literal(m_util.str.mk_contains(t, s));
-        literal eq_empty = mk_eq_empty(s);
+        literal s_eq_empty = mk_eq_empty(s);
         add_axiom(cnt,  mk_eq(i, minus_one, false));
-        add_axiom(~eq_empty, mk_eq(i, zero, false));
-        add_axiom(eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false));
-        add_axiom(~cnt, eq_empty, mk_eq(t, xsy, false));
+        add_axiom(~s_eq_empty, mk_eq(i, zero, false));
+        add_axiom(s_eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false));
+        add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
+        add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false));
         tightest_prefix(s, x, ~cnt);
     }
     else {
@@ -1722,7 +1696,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
         // 0 <= offset & offset < len(t) & indexof(y,s,0) >= 0 = -1 =>
         //                  -1 = indexof(y,s,0) + offset = indexof(t, s, offset)
 
-        add_axiom(~offset_ge_0, offset_ge_len, mk_eq(t, mk_concat(x, y), false));
+        add_axiom(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y)));
         add_axiom(~offset_ge_0, offset_ge_len, mk_eq(m_util.str.mk_length(x), offset, false));
         add_axiom(~offset_ge_0, offset_ge_len,
                   ~mk_eq(indexof0, minus_one, false), mk_eq(i, minus_one, false));
@@ -1743,14 +1717,14 @@ void theory_seq::add_indexof_axiom(expr* i) {
 void theory_seq::add_replace_axiom(expr* r) {
     expr* a, *s, *t;
     VERIFY(m_util.str.is_replace(r, a, s, t));
-    expr_ref x  = mk_skolem(m_contains_left, a, s);
-    expr_ref y  = mk_skolem(m_contains_right, a, s);
+    expr_ref x  = mk_skolem(m_indexof_left, a, s);
+    expr_ref y  = mk_skolem(m_indexof_right, a, s);
     expr_ref xty = mk_concat(x, t, y);
     expr_ref xsy = mk_concat(x, s, y);
     literal cnt = mk_literal(m_util.str.mk_contains(a ,s));
-    add_axiom(cnt,  mk_eq(r, a, false));
-    add_axiom(~cnt, mk_eq(a, xsy, false));
-    add_axiom(~cnt, mk_eq(r, xty, false));
+    add_axiom(cnt,  mk_seq_eq(r, a));
+    add_axiom(~cnt, mk_seq_eq(a, xsy));
+    add_axiom(~cnt, mk_seq_eq(r, xty));
     tightest_prefix(s, x, ~cnt);
 }
 
@@ -1965,12 +1939,16 @@ bool theory_seq::get_length(expr* e, rational& val) {
 
   let e = extract(s, i, l)
 
-  0 <= i < len(s) -> prefix(xe,s) & len(x) = i
-  0 <= i < len(s) & l >= len(s) - i -> len(e) = len(s) - i
-  0 <= i < len(s) & 0 <= l < len(s) - i -> len(e) = l
-  0 <= i < len(s) & l < 0 -> len(e) = 0
-  *  i < 0 -> e = s
-  *  i >= len(s) -> e = empty
+  0 <= i <= len(s) -> prefix(xe,s) 
+  0 <= i <= len(s) -> len(x) = i
+  0 <= i <= len(s) & 0 <= l <= len(s) - i -> len(e) = l
+  0 <= i <= len(s) & len(s) < l + i  -> len(e) = len(s) - i
+  0 <= i <= len(s) & l < 0 -> len(e) = 0
+  *  i < 0 -> e = empty
+  *  i > len(s) -> e = empty
+
+ 
+
 */
 
 void theory_seq::add_extract_axiom(expr* e) {
@@ -1984,15 +1962,16 @@ void theory_seq::add_extract_axiom(expr* e) {
     expr_ref xe = mk_concat(x, e);
     expr_ref zero(m_autil.mk_int(0), m);
 
-    literal i_ge_0  = mk_literal(m_autil.mk_ge(i, zero));
-    literal i_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
-    literal li_ge_ls = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
+    literal i_ge_0    = mk_literal(m_autil.mk_ge(i, zero));
+    literal i_le_ls   = mk_literal(m_autil.mk_le(mk_sub(i, ls), zero));
+    literal li_ge_ls  = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
     literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
 
-    add_axiom(~i_ge_0, i_ge_ls, mk_literal(m_util.str.mk_prefix(xe, s)));
-    add_axiom(~i_ge_0, i_ge_ls, mk_eq(lx, i, false));
-    add_axiom(~i_ge_0, i_ge_ls, ~li_ge_ls, mk_eq(le, l, false));
-    add_axiom(~i_ge_0, i_ge_ls, l_ge_zero, mk_eq(le, zero, false));
+    add_axiom(~i_ge_0, ~i_le_ls, mk_literal(m_util.str.mk_prefix(xe, s)));
+    add_axiom(~i_ge_0, ~i_le_ls, mk_eq(lx, i, false));
+    add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_zero, ~li_ge_ls, mk_eq(le, l, false));
+    add_axiom(~i_ge_0, ~i_le_ls, li_ge_ls, mk_eq(le, mk_sub(ls, i), false));
+    add_axiom(~i_ge_0, ~i_le_ls, l_ge_zero, mk_eq(le, zero, false));
 }
 
 /*
@@ -2016,7 +1995,7 @@ void theory_seq::add_at_axiom(expr* e) {
     literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
     literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
 
-    add_axiom(~i_ge_0, i_ge_len_s, mk_eq(s, xey, false));
+    add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey));
     add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false));
     add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false));
 }
@@ -2075,10 +2054,10 @@ literal theory_seq::mk_literal(expr* _e) {
     return ctx.get_literal(e);
 }
 
-literal theory_seq::mk_equals(expr* a, expr* b) {
-    literal lit = mk_eq(a, b, false);
-    get_context().force_phase(lit);
-    return lit;
+
+literal theory_seq::mk_seq_eq(expr* a, expr* b) {
+    SASSERT(m_util.is_seq(a));
+    return mk_literal(mk_skolem(symbol("seq.eq"), a, b, 0, m.mk_bool_sort()));
 }
 
 literal theory_seq::mk_eq_empty(expr* _e) {
@@ -2086,26 +2065,36 @@ literal theory_seq::mk_eq_empty(expr* _e) {
     SASSERT(m_util.is_seq(e));
     expr_ref emp(m);
     zstring s;
-    if (m_util.str.is_string(e, s)) {
-        if (s.length() == 0) {
-            return true_literal;
+    if (m_util.str.is_empty(e)) {
+        return true_literal;
+    }
+    expr_ref_vector concats(m);
+    m_util.str.get_concat(e, concats);
+    for (unsigned i = 0; i < concats.size(); ++i) {
+        if (m_util.str.is_unit(concats[i].get())) {
+            return false_literal;
         }
-        else {
+        if (m_util.str.is_string(concats[i].get(), s) && s.length() > 0) {
             return false_literal;
         }
     }
     emp = m_util.str.mk_empty(m.get_sort(e));
-    return mk_equals(e, emp);
+
+
+    literal lit = mk_eq(e, emp, false);
+    get_context().force_phase(lit);
+    return lit;
 }
 
-void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) {
+void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, literal l5) {
     context& ctx = get_context();
     literal_vector lits;
-    if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal) return;
+    if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal || l5 == true_literal) return;
     if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); }
     if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); }
     if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); }
     if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); }
+    if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); }
     TRACE("seq", ctx.display_literals_verbose(tout << "axiom: ", lits.size(), lits.c_ptr()); tout << "\n";);
     m_new_propagation = true;
     ++m_stats.m_add_axiom;
@@ -2162,6 +2151,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     expr* e = ctx.bool_var2expr(v);
     expr* e1, *e2;
     expr_ref f(m);
+    bool change = false;
     literal lit(v, !is_true);
 
     if (m_util.str.is_prefix(e, e1, e2)) {
@@ -2171,11 +2161,14 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             propagate_eq(lit, f, e2, true);
         }
         else {
-            // !prefix(e1,e2) => e1 != ""
+#if 0
+            propagate_not_prefix(e);
+#else
             propagate_non_empty(lit, e1);
-            if (add_prefix2prefix(e)) {
+            if (add_prefix2prefix(e, change)) {
                 add_atom(e);
             }
+#endif
         }
     }
     else if (m_util.str.is_suffix(e, e1, e2)) {
@@ -2185,6 +2178,10 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             propagate_eq(lit, f, e2, true);
         }
         else {
+#if 1
+            propagate_not_suffix(e);
+
+#else
             // lit => e1 != empty
             propagate_non_empty(lit, e1);
 
@@ -2194,9 +2191,11 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             f = mk_concat(f1, m_util.str.mk_unit(f2));
             propagate_eq(lit, e1, f, true);
 
-            if (add_suffix2suffix(e)) {
+            TRACE("seq", tout << "suffix: " << f << " = " << mk_pp(e1, m) << "\n";);
+            if (add_suffix2suffix(e, change)) {
                 add_atom(e);
             }
+#endif
         }
     }
     else if (m_util.str.is_contains(e, e1, e2)) {
@@ -2209,7 +2208,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
         else if (!canonizes(false, e)) {
             propagate_non_empty(lit, e2);
             propagate_lit(0, 1, &lit, ~mk_literal(m_util.str.mk_prefix(e2, e1)));
-            if (add_contains2contains(e)) {
+            if (add_contains2contains(e, change)) {
                 add_atom(e);
             }
         }
@@ -2217,7 +2216,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (is_accept(e)) {
         if (is_true) {
             propagate_acc_rej_length(lit, e);
-            if (add_accept2step(e)) {
+            if (add_accept2step(e, change)) {
                 add_atom(e);
             }
         }
@@ -2231,11 +2230,16 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (is_step(e)) {
         if (is_true) {
             propagate_step(lit, e);
-            if (add_step2accept(e)) {
+            if (add_step2accept(e, change)) {
                 add_atom(e);
             }
         }
     }
+    else if (is_eq(e, e1, e2)) {
+        if (is_true) {
+            propagate_eq(lit, e1, e2, true);
+        }
+    }
     else if (m_util.str.is_in_re(e)) {
         propagate_in_re(e, is_true);
     }
@@ -2277,13 +2281,53 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     m_rewrite(eq);
     if (!m.is_false(eq)) {
         TRACE("seq", tout << "new disequality: " << eq << "\n";);
-        literal lit = ~mk_eq(e1, e2, false);
-        //SASSERT(get_context().get_assignment(lit) == l_true);
-        dependency* dep = m_dm.mk_leaf(assumption(lit));
-        m_nqs.push_back(ne(e1, e2, dep));
-        solve_nqs(m_nqs.size() - 1);
+
+        literal lit = mk_eq(e1, e2, false);
+
+        // propagate x != "" into x = (++ (unit (nth x 0) (tail x 0)))
+        if (m_util.str.is_empty(e2)) {
+            std::swap(e1, e2);
+        }
+        if (false && m_util.str.is_empty(e1)) {
+            expr_ref head(m), tail(m), conc(m);
+            mk_decompose(e2, head, tail);
+            conc = mk_concat(head, tail);
+            propagate_eq(~lit, e2, conc, true);
+        }
+#if 0
+        // (e1 = "" & e2 = xdz) or (e2 = "" & e1 = xcy) or (e1 = xcy & e2 = xdz & c != d) or (e1 = x & e2 = xdz) or (e2 = x & e1 = xcy)
+        // e1 = "" or e1 = xcy or e1 = x
+        // e2 = "" or e2 = xdz or e2 = x
+        // e1 = xcy or e2 = xdz
+        // c != d
+
+        literal lit = mk_seq_eq(e1, e2);
+        sort* char_sort = 0;
+        expr_ref emp(m);
+        VERIFY(m_util.is_seq(m.get_sort(e1), char_sort));
+        emp = m_util.str.mk_empty(m.get_sort(e1));
+
+        expr_ref x = mk_skolem(symbol("seq.ne.x"), e1, e2);
+        expr_ref y = mk_skolem(symbol("seq.ne.y"), e1, e2);
+        expr_ref z = mk_skolem(symbol("seq.ne.z"), e1, e2);
+        expr_ref c = mk_skolem(symbol("seq.ne.c"), e1, e2, 0, char_sort);
+        expr_ref d = mk_skolem(symbol("seq.ne.d"), e1, e2, 0, char_sort);
+        literal e1_is_emp = mk_seq_eq(e1, emp);
+        literal e2_is_emp = mk_seq_eq(e2, emp);
+        literal e1_is_xcy = mk_seq_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y));
+        literal e2_is_xdz = mk_seq_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z));
+        add_axiom(lit, e1_is_emp, e1_is_xcy, mk_seq_eq(e1, x));
+        add_axiom(lit, e2_is_emp, e2_is_xdz, mk_seq_eq(e2, x));
+        add_axiom(lit, e1_is_xcy, e2_is_xdz);
+        add_axiom(lit, ~mk_eq(c, d, false));
+#else
+        else {
+            dependency* dep = m_dm.mk_leaf(assumption(~lit));
+            m_nqs.push_back(ne(e1, e2, dep));
+            solve_nqs(m_nqs.size() - 1);
+        }
+#endif
     }
-    // add solution for variable that is non-empty?
 }
 
 void theory_seq::push_scope_eh() {
@@ -2444,7 +2488,7 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
    acc(s, idx, re, i) ->  \/ step(s, idx, re, i, j, t)                if i is non-final
    acc(s, idx, re, i) -> len(s) <= idx \/ step(s, idx, re, i, j, t)   if i is final
 */
-bool theory_seq::add_accept2step(expr* acc) {
+bool theory_seq::add_accept2step(expr* acc, bool& change) {
     context& ctx = get_context();
 
     TRACE("seq", tout << mk_pp(acc, m) << "\n";);
@@ -2467,9 +2511,10 @@ bool theory_seq::add_accept2step(expr* acc) {
     if (aut->is_final_state(src)) {
         lits.push_back(mk_literal(m_autil.mk_le(len, idx)));
         switch (ctx.get_assignment(lits.back())) {
-        case l_true:
+        case l_true:            
             return false;
         case l_undef:
+            change = true;
             ctx.force_phase(lits.back());
             return true;
         default:
@@ -2497,6 +2542,7 @@ bool theory_seq::add_accept2step(expr* acc) {
             break;
         }
     }
+    change = true;
     if (has_undef && mvs.size() == 1) {
         literal lit = lits.back();
         lits.pop_back();
@@ -2523,7 +2569,7 @@ bool theory_seq::add_accept2step(expr* acc) {
    acc(s, idx, re, i) & step(s, idx, re, i, j, t) => acc(s, idx + 1, re, j)
 */
 
-bool theory_seq::add_step2accept(expr* step) {
+bool theory_seq::add_step2accept(expr* step, bool& change) {
     context& ctx = get_context();
     SASSERT(ctx.get_assignment(step) == l_true);
     expr* re, *_acc, *s, *idx, *i, *j;
@@ -2533,8 +2579,10 @@ bool theory_seq::add_step2accept(expr* step) {
     case l_false:
         break;
     case l_undef:
+        change = true;
         return true;
     case l_true: {
+        change = true;
         rational r;
         VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned());
         expr_ref idx1(m_autil.mk_int(r.get_unsigned() + 1), m);
@@ -2570,7 +2618,7 @@ Recall we also have:
    rej(s, idx, re, i) -> len(s) > idx     if i is final
 
 */
-bool theory_seq::add_reject2reject(expr* rej) {
+bool theory_seq::add_reject2reject(expr* rej, bool& change) {
     context& ctx = get_context();
     SASSERT(ctx.get_assignment(rej) == l_true);
     expr* s, *idx, *re;
@@ -2590,7 +2638,7 @@ bool theory_seq::add_reject2reject(expr* rej) {
     case l_true:
         return false;
     case l_undef:
-        ctx.force_phase(len_le_idx);
+        ctx.force_phase(len_le_idx);       
         return true;
     default:
         break;
@@ -2613,6 +2661,7 @@ bool theory_seq::add_reject2reject(expr* rej) {
         }
         eqs.push_back(eq);
     }
+    change = true;
     if (has_undef) {
         return true;
     }
@@ -2627,10 +2676,71 @@ bool theory_seq::add_reject2reject(expr* rej) {
     return false;
 }
 
+/*
+  !prefix(e1,e2) => e1 != ""
+  !prefix(e1,e2) => e2 = "" or e1 = xcy & (e2 = xdz & c != d or x = e2)
+*/
+
+void theory_seq::propagate_not_prefix(expr* e) {
+    context& ctx = get_context();
+    expr* e1, *e2;
+    VERIFY(m_util.str.is_prefix(e, e1, e2));
+    literal lit = ctx.get_literal(e);
+    SASSERT(ctx.get_assignment(lit) == l_false);
+    if (canonizes(false, e)) {
+        return;
+    }
+    propagate_non_empty(~lit, e1);
+    expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
+    literal e2_is_emp = mk_seq_eq(e2, emp);
+    sort* char_sort = 0;
+    VERIFY(m_util.is_seq(m.get_sort(e1), char_sort));
+    expr_ref x = mk_skolem(symbol("seq.prefix.x"), e1, e2);
+    expr_ref y = mk_skolem(symbol("seq.prefix.y"), e1, e2);
+    expr_ref z = mk_skolem(symbol("seq.prefix.z"), e1, e2);
+    expr_ref c = mk_skolem(symbol("seq.prefix.c"), e1, e2, 0, char_sort);
+    expr_ref d = mk_skolem(symbol("seq.prefix.d"), e1, e2, 0, char_sort);
+    add_axiom(lit, e2_is_emp, mk_seq_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y)));
+    add_axiom(lit, e2_is_emp, mk_seq_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z)), mk_seq_eq(e2, x));
+    add_axiom(lit, e2_is_emp, ~mk_eq(c, d, false), mk_seq_eq(e2, x));
+}
+
+/*
+  !suffix(e1,e2) => e1 != ""
+  !suffix(e1,e2) => e2 = "" or e1 = ycx & (e2 = zdx & c != d or x = e2)
+ */
+
+
+void theory_seq::propagate_not_suffix(expr* e) {
+    context& ctx = get_context();
+    expr* e1, *e2;
+    VERIFY(m_util.str.is_suffix(e, e1, e2));
+    literal lit = ctx.get_literal(e);
+    SASSERT(ctx.get_assignment(lit) == l_false);
+    if (canonizes(false, e)) {
+        return;
+    }
+    propagate_non_empty(~lit, e1);
+    
+    expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
+    literal e2_is_emp = mk_seq_eq(e2, emp);
+    sort* char_sort = 0;
+    VERIFY(m_util.is_seq(m.get_sort(e1), char_sort));
+    expr_ref x = mk_skolem(symbol("seq.suffix.x"), e1, e2);
+    expr_ref y = mk_skolem(symbol("seq.suffix.y"), e1, e2);
+    expr_ref z = mk_skolem(symbol("seq.suffix.z"), e1, e2);
+    expr_ref c = mk_skolem(symbol("seq.suffix.c"), e1, e2, 0, char_sort);
+    expr_ref d = mk_skolem(symbol("seq.suffix.d"), e1, e2, 0, char_sort);
+    add_axiom(lit, e2_is_emp, mk_seq_eq(e1, mk_concat(y, m_util.str.mk_unit(c), x)));
+    add_axiom(lit, e2_is_emp, mk_seq_eq(e2, mk_concat(z, m_util.str.mk_unit(d), x)), mk_seq_eq(e2, x));
+    add_axiom(lit, e2_is_emp, ~mk_eq(c, d, false), mk_seq_eq(e2, x));
+}
+
+
 /*
   !prefix -> e2 = emp \/ nth(e1,0) != nth(e2,0) \/ !prefix(tail(e1),tail(e2))
 */
-bool theory_seq::add_prefix2prefix(expr* e) {
+bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
     context& ctx = get_context();
     expr* e1, *e2;
     VERIFY(m_util.str.is_prefix(e, e1, e2));
@@ -2638,46 +2748,70 @@ bool theory_seq::add_prefix2prefix(expr* e) {
     if (canonizes(false, e)) {
         return false;
     }
-    expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
+    expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m);
+
+    TRACE("seq", tout << mk_pp(e, m) << "\n";);
+
     literal e2_is_emp = mk_eq_empty(e2);
     switch (ctx.get_assignment(e2_is_emp)) {
     case l_true:
+        TRACE("seq", tout << mk_pp(e2, m) << " = empty\n";);
         return false; // done
     case l_undef:
+        // ctx.force_phase(e2_is_emp);
+        TRACE("seq", tout << mk_pp(e2, m) << " ~ empty\n";);
         return true;  // retry
     default:
         break;
     }
 
-    expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m);
-    mk_decompose(e1, head1, tail1);
     mk_decompose(e2, head2, tail2);
     conc = mk_concat(head2, tail2);
     propagate_eq(~e2_is_emp, e2, conc, true);
 
+    literal e1_is_emp = mk_eq_empty(e1);
+    switch (ctx.get_assignment(e1_is_emp)) {
+    case l_true:        
+        TRACE("seq", tout << mk_pp(e1, m) << " = empty\n";);
+        return false; // done
+    case l_undef:        
+        TRACE("seq", tout << mk_pp(e1, m) << " ~ empty\n";);
+        return true;  // retry
+    default:
+        break;
+    }
+
+    mk_decompose(e1, head1, tail1);
+    conc = mk_concat(head1, tail1);
+    propagate_eq(~e1_is_emp, e1, conc, true);
+
+
     literal lit = mk_eq(head1, head2, false);
     switch (ctx.get_assignment(lit)) {
-    case l_true: {
-        literal_vector lits;
-        lits.push_back(~ctx.get_literal(e));
-        lits.push_back(~e2_is_emp);
-        lits.push_back(lit);
-        propagate_lit(0, lits.size(), lits.c_ptr(), ~mk_literal(m_util.str.mk_prefix(tail1, tail2)));
-        return false;
-    }
+    case l_true: 
+        break;
     case l_false:
+        TRACE("seq", tout << head1 << " = " << head2 << "\n";);
         return false;
     case l_undef:
         ctx.force_phase(~lit);
+        TRACE("seq", tout << head1 << " ~ " << head2 << "\n";);
         return true;
     }
-    return true;
+    change = true;
+    literal_vector lits;
+    lits.push_back(~ctx.get_literal(e));
+    lits.push_back(~e2_is_emp);
+    lits.push_back(lit);
+    propagate_lit(0, lits.size(), lits.c_ptr(), ~mk_literal(m_util.str.mk_prefix(tail1, tail2)));
+    TRACE("seq", tout << "saturate: " << tail1 << " = " << tail2 << "\n";);
+    return false;
 }
 
 /*
   !suffix(e1, e2) -> e2 = emp \/ last(e1) != last(e2) \/ !suffix(first(e1), first(e2))
  */
-bool theory_seq::add_suffix2suffix(expr* e) {
+bool theory_seq::add_suffix2suffix(expr* e, bool& change) {
     context& ctx = get_context();
     expr* e1, *e2;
     VERIFY(m_util.str.is_suffix(e, e1, e2));
@@ -2686,14 +2820,11 @@ bool theory_seq::add_suffix2suffix(expr* e) {
         return false;
     }
 
-    expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
     literal e2_is_emp = mk_eq_empty(e2);
     switch (ctx.get_assignment(e2_is_emp)) {
     case l_true:
-        TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(e2, m) << " is empty\n";);
         return false; // done
-    case l_undef:
-        TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(e2, m) << " is unassigned\n";);
+    case l_undef:        
         ctx.force_phase(e2_is_emp);
         return true;  // retry
     case l_false:
@@ -2701,24 +2832,37 @@ bool theory_seq::add_suffix2suffix(expr* e) {
     }
     expr_ref first2 = mk_first(e2);
     expr_ref last2  = mk_last(e2);
+    expr_ref conc2 = mk_concat(first2, m_util.str.mk_unit(last2));
+    propagate_eq(~e2_is_emp, e2, conc2, true);
+
+    literal e1_is_emp = mk_eq_empty(e1);
+    switch (ctx.get_assignment(e1_is_emp)) {
+    case l_true:
+        return false; // done
+    case l_undef:
+        ctx.force_phase(e1_is_emp);
+        return true;  // retry
+    case l_false:
+        break;
+    }
     expr_ref first1 = mk_first(e1);
     expr_ref last1  = mk_last(e1);
-    expr_ref conc = mk_concat(first2, m_util.str.mk_unit(last2));
-    propagate_eq(~e2_is_emp, e2, conc, true);
+    expr_ref conc1 = mk_concat(first1, m_util.str.mk_unit(last1));
+    propagate_eq(~e1_is_emp, e1, conc1, true);
+
 
     literal last_eq = mk_eq(last1, last2, false);
     switch (ctx.get_assignment(last_eq)) {
     case l_false:
-        TRACE("seq", tout << mk_pp(e, m) << " " << last1 << " = " << last2 << " is false\n";);
         return false; // done
     case l_undef:
-        TRACE("seq", tout << mk_pp(e, m) << " " << last1 << " = " << last2 << " is unassigned\n";);
         ctx.force_phase(~last_eq);
         return true;
     case l_true:
         break;
     }
 
+    change = true;
     literal_vector lits;
     lits.push_back(~ctx.get_literal(e));
     lits.push_back(~e2_is_emp);
@@ -2750,7 +2894,7 @@ bool theory_seq::canonizes(bool sign, expr* e) {
    !contains(e1, e2) -> e1 = emp \/ !contains(tail(e1), e2)
  */
 
-bool theory_seq::add_contains2contains(expr* e) {
+bool theory_seq::add_contains2contains(expr* e, bool& change) {
     context& ctx = get_context();
     expr* e1, *e2;
     VERIFY(m_util.str.is_contains(e, e1, e2));
@@ -2758,19 +2902,25 @@ bool theory_seq::add_contains2contains(expr* e) {
     if (canonizes(false, e)) {
         return false;
     }
-    expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
-
-    switch (assume_equality(e1, emp)) {
+    
+    literal e1_is_emp = mk_eq_empty(e1);
+    switch (ctx.get_assignment(e1_is_emp)) {
     case l_true:
         return false; // done
     case l_undef:
+        ctx.force_phase(e1_is_emp);
         return true;  // retry
     default:
         break;
     }
-    expr_ref head(m), tail(m);
+    change = true;
+    expr_ref head(m), tail(m), conc(m);
     mk_decompose(e1, head, tail);
-    literal lits[2] = { ~ctx.get_literal(e), ~mk_eq(e1, emp, false) };
+    
+    conc = mk_concat(head, tail);
+    propagate_eq(~e1_is_emp, e1, conc, true);
+
+    literal lits[2] = { ~ctx.get_literal(e), ~e1_is_emp };
     propagate_lit(0, 2, lits, ~mk_literal(m_util.str.mk_contains(tail, e2)));
     return false;
 }
@@ -2782,33 +2932,49 @@ bool theory_seq::propagate_automata() {
     }
     m_trail_stack.push(value_trail<theory_seq, unsigned>(m_atoms_qhead));
     ptr_vector<expr> re_add;
+    bool change = false;
     while (m_atoms_qhead < m_atoms.size() && !ctx.inconsistent()) {
         expr* e = m_atoms[m_atoms_qhead];
         TRACE("seq", tout << mk_pp(e, m) << "\n";);
         bool reQ = false;
         if (is_accept(e)) {
-            reQ = add_accept2step(e);
+            reQ = add_accept2step(e, change);
         }
         else if (is_reject(e)) {
-            reQ = add_reject2reject(e);
+            reQ = add_reject2reject(e, change);
         }
         else if (is_step(e)) {
-            reQ = add_step2accept(e);
+            reQ = add_step2accept(e, change);
         }
         else if (m_util.str.is_prefix(e)) {
-            reQ = add_prefix2prefix(e);
+            reQ = add_prefix2prefix(e, change);
         }
         else if (m_util.str.is_suffix(e)) {
-            reQ = add_suffix2suffix(e);
+            reQ = add_suffix2suffix(e, change);
         }
         else if (m_util.str.is_contains(e)) {
-            reQ = add_contains2contains(e);
+            reQ = add_contains2contains(e, change);
         }
         if (reQ) {
             re_add.push_back(e);
+            change = true;
         }
         ++m_atoms_qhead;
     }
     m_atoms.append(re_add);
-    return true;
+    return change || get_context().inconsistent();
+}
+
+void theory_seq::get_concat(expr* e, ptr_vector<expr>& concats) {
+    expr* e1, *e2;
+    while (true) {
+        e = m_rep.find(e);
+        if (m_util.str.is_concat(e, e1, e2)) {
+            get_concat(e1, concats);
+            e = e2;
+            continue;
+        }
+        concats.push_back(e);        
+        return;
+    }
 }
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 8ad9e7caf..7183b2950 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -45,6 +45,8 @@ namespace smt {
         typedef std::pair<expr*, dependency*> expr_dep;
         typedef obj_map<expr, expr_dep> eqdep_map_t; 
 
+        class seq_value_proc;
+
         // cache to track evaluations under equalities
         class eval_cache {
             eqdep_map_t             m_map;
@@ -138,8 +140,7 @@ namespace smt {
             m_util.str.get_concat(l, ls);
             m_util.str.get_concat(r, rs);
             return eq(m_eq_id++, ls, rs, dep);
-        }
-
+        }        
 
         class ne {            
             vector<expr_ref_vector>  m_lhs;
@@ -355,6 +356,7 @@ namespace smt {
         bool add_solution(expr* l, expr* r, dependency* dep);
         bool is_nth(expr* a) const;
         bool is_tail(expr* a, expr*& s, unsigned& idx) const;
+        bool is_eq(expr* e, expr*& a, expr*& b) const; 
         expr_ref mk_nth(expr* s, expr* idx);
         expr_ref mk_last(expr* e);
         expr_ref mk_first(expr* e);
@@ -369,7 +371,7 @@ namespace smt {
         // terms whose meaning are encoded using axioms.
         void enque_axiom(expr* e);
         void deque_axiom(expr* e);
-        void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal);        
+        void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);        
         void add_indexof_axiom(expr* e);
         void add_replace_axiom(expr* e);
         void add_extract_axiom(expr* e);
@@ -385,7 +387,7 @@ namespace smt {
         void add_in_re_axiom(expr* n);
         literal mk_literal(expr* n);
         literal mk_eq_empty(expr* n);
-        literal mk_equals(expr* a, expr* b);
+        literal mk_seq_eq(expr* a, expr* b);
         void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
         expr_ref mk_sub(expr* a, expr* b);
         enode* ensure_enode(expr* a);
@@ -421,12 +423,14 @@ namespace smt {
         bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
         bool is_step(expr* e) const;
         void propagate_step(literal lit, expr* n);
-        bool add_reject2reject(expr* rej);
-        bool add_accept2step(expr* acc);       
-        bool add_step2accept(expr* step);
-        bool add_prefix2prefix(expr* e);
-        bool add_suffix2suffix(expr* e);
-        bool add_contains2contains(expr* e);
+        bool add_reject2reject(expr* rej, bool& change);
+        bool add_accept2step(expr* acc, bool& change);       
+        bool add_step2accept(expr* step, bool& change);
+        bool add_prefix2prefix(expr* e, bool& change);
+        bool add_suffix2suffix(expr* e, bool& change);
+        bool add_contains2contains(expr* e, bool& change);
+        void propagate_not_prefix(expr* e);
+        void propagate_not_suffix(expr* e);
         void ensure_nth(literal lit, expr* s, expr* idx);
         bool canonizes(bool sign, expr* e);
         void propagate_non_empty(literal lit, expr* s);
diff --git a/src/tactic/smtlogics/quant_tactics.h b/src/tactic/smtlogics/quant_tactics.h
index 3da05a0f2..b78730236 100644
--- a/src/tactic/smtlogics/quant_tactics.h
+++ b/src/tactic/smtlogics/quant_tactics.h
@@ -32,4 +32,17 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_lia_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_lira_tactic(ast_manager & m, params_ref const & p);
 
+/*
+  ADD_TACTIC("ufnia", "builtin strategy for solving UFNIA problems.", "mk_ufnia_tactic(m, p)")
+  ADD_TACTIC("uflra", "builtin strategy for solving UFLRA problems.", "mk_uflra_tactic(m, p)")
+  ADD_TACTIC("auflia", "builtin strategy for solving AUFLIA problems.", "mk_auflia_tactic(m, p)")
+  ADD_TACTIC("auflira", "builtin strategy for solving AUFLIRA problems.", "mk_auflira_tactic(m, p)")
+  ADD_TACTIC("aufnira", "builtin strategy for solving AUFNIRA problems.", "mk_aufnira_tactic(m, p)")
+  ADD_TACTIC("lra", "builtin strategy for solving LRA problems.", "mk_lra_tactic(m, p)")
+  ADD_TACTIC("lia", "builtin strategy for solving LIA problems.", "mk_lia_tactic(m, p)")
+  ADD_TACTIC("lira", "builtin strategy for solving LIRA problems.", "mk_lira_tactic(m, p)")
+
+*/
+
+
 #endif