diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 00b4371d9..2db2391d9 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -520,20 +520,10 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), a);
         return BR_REWRITE3;
     }
-    // TBD concatenation is right-associative
-    expr* a1, *a2, *b1, *b2;
-    if (m_util.str.is_concat(a, a1, a2) && 
-        m_util.str.is_concat(b, b1, b2) && a2 == b2) {
-        result = m_util.str.mk_suffix(a1, b1);
-        return BR_REWRITE1;
-    }
-    if (m_util.str.is_concat(b, b1, b2) && b2 == a) {
-        result = m().mk_true();
-        return BR_DONE;
-    }
+
     bool isc1 = false;
     bool isc2 = false;
-    
+    expr* a1, *a2, *b1, *b2;
     if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
         isc1 = true;
     }
@@ -593,6 +583,37 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
             }            
         }
     }
+    expr_ref_vector as(m()), bs(m());
+    m_util.str.get_concat(a, as);
+    m_util.str.get_concat(b, bs);
+    bool change = false;
+    while (as.size() > 0 && bs.size() > 0 && as.back() == bs.back()) {
+        as.pop_back();
+        bs.pop_back();
+        change = true;
+    }
+    if (as.size() > 0 && bs.size() > 0 && m().is_value(as.back()) && m().is_value(bs.back())) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    if (change) {
+        // suffix("", bs) <- true
+        if (as.empty()) {
+            result = m().mk_true();
+            return BR_DONE;
+        }
+        // suffix(as, "") iff as = ""
+        if (bs.empty()) {            
+            for (unsigned j = 0; j < as.size(); ++j) {
+                bs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
+            }
+            result = mk_and(bs);
+            return BR_REWRITE3;
+        }
+        result = m_util.str.mk_suffix(m_util.str.mk_concat(as.size(), as.c_ptr()),
+                                     m_util.str.mk_concat(bs.size(), bs.c_ptr()));
+        return BR_DONE;
+    }
 
     return BR_FAILED;
 }
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 70ee4298b..c3f882e8d 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -25,7 +25,6 @@ Revision History:
 zstring::zstring(encoding enc): m_encoding(enc) {}
 
 zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
-    // TBD: epply decoding
     while (*s) {
         m_buffer.push_back(*s);
         ++s;
@@ -81,6 +80,7 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
     return result;
 }
 
+// TBD: SMT-LIB 2.5 strings don't have escape characters other than "
 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","^\\","^]","^^","^_"};
  
diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp
index e76b3a25b..3f5c2b78f 100644
--- a/src/muz/rel/dl_mk_simple_joins.cpp
+++ b/src/muz/rel/dl_mk_simple_joins.cpp
@@ -273,6 +273,7 @@ namespace datalog {
             */
         void register_pair(app * t1, app * t2, rule * r, const var_idx_set & non_local_vars) {
             SASSERT(t1!=t2);
+            std::cout << "insert: " << mk_pp(t1, m) << " - " << mk_pp(t2, m) << "\n";
             cost_map::entry * e = m_costs.insert_if_not_there2(get_key(t1, t2), 0);
             pair_info * & ptr_inf = e->get_data().m_value;
             if (ptr_inf==0) {
@@ -306,6 +307,7 @@ namespace datalog {
         }
 
         void remove_rule_from_pair(app_pair key, rule * r, unsigned original_len) {
+            std::cout << "remove: " << mk_pp(key.first, m) << " - " << mk_pp(key.second, m) << "\n";
             pair_info * ptr = &get_pair(key);
             if (ptr->remove_rule(r, original_len)) {
                 SASSERT(ptr->m_rules.empty());
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 954baa4c6..69ae25aba 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -150,6 +150,7 @@ void theory_seq::exclusion_table::display(std::ostream& out) const {
     }
 }
 
+
 theory_seq::theory_seq(ast_manager& m):
     theory(m.mk_family_id("seq")), 
     m(m),
@@ -372,6 +373,7 @@ bool theory_seq::propagate_length_coherence(expr* e) {
         expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m);
         expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m);     
         add_axiom(~mk_literal(high1), mk_literal(high2));
+        m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
     }
 
     return true;
@@ -1048,12 +1050,18 @@ app* theory_seq::mk_value(app* e) {
         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));
+            unsigned v = val.get_unsigned();
+            if ((0 <= v && v < 32) || v == 127) {
+                result = m_util.str.mk_unit(result);                
+            }
+            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()));
             }
-            result = m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr()));
         }
         else {
             result = m_util.str.mk_unit(result);
@@ -1113,7 +1121,7 @@ theory_var theory_seq::mk_var(enode* n) {
 }
 
 bool theory_seq::can_propagate() {
-    return m_axioms_head < m_axioms.size();
+    return m_axioms_head < m_axioms.size() || !m_replay.empty();
 }
 
 expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
@@ -1177,6 +1185,11 @@ void theory_seq::propagate() {
         deque_axiom(e);
         ++m_axioms_head;
     }
+    while (!m_replay.empty() && !ctx.inconsistent()) {
+        (*m_replay[m_replay.size()-1])(*this);
+        TRACE("seq", tout << "replay: " << ctx.get_scope_level() << "\n";);
+        m_replay.pop_back();
+    }
 }
 
 void theory_seq::enque_axiom(expr* e) {
@@ -1733,7 +1746,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
         else {
             // !prefix(e1,e2) => e1 != ""
             propagate_non_empty(lit, e1);
-            add_atom(e);
+            if (add_prefix2prefix(e)) {
+                add_atom(e);
+            }
         }
     }
     else if (m_util.str.is_suffix(e, e1, e2)) {
@@ -1752,7 +1767,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             f = m_util.str.mk_concat(f1, m_util.str.mk_unit(f2));
             propagate_eq(lit, e1, f, true);
 
-            add_atom(e);
+            if (add_suffix2suffix(e)) {
+                add_atom(e);
+            }
         }
     }
     else if (m_util.str.is_contains(e, e1, e2)) {
@@ -1765,13 +1782,17 @@ 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)));
-            add_atom(e);
+            if (add_contains2contains(e)) {
+                add_atom(e);
+            }
         }
     }
     else if (is_accept(e)) {
         if (is_true) {
             propagate_acc_rej_length(lit, e);
-            add_atom(e);
+            if (add_accept2step(e)) {
+                add_atom(e);
+            }
         }
     }
     else if (is_reject(e)) {
@@ -1783,7 +1804,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (is_step(e)) {
         if (is_true) {
             propagate_step(lit, e);
-            add_atom(e);
+            if (add_step2accept(e)) {
+                add_atom(e);
+            }
         }
     }
     else if (m_util.str.is_in_re(e)) {
@@ -1979,10 +2002,10 @@ 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) ->  \/ 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
 */
-void theory_seq::add_accept2step(expr* acc) {
+bool theory_seq::add_accept2step(expr* acc) {
     context& ctx = get_context();
     SASSERT(ctx.get_assignment(acc) == l_true);
     expr *e, * idx, *re;
@@ -1990,7 +2013,9 @@ void theory_seq::add_accept2step(expr* acc) {
     unsigned src;
     eautomaton* aut = 0;
     VERIFY(is_accept(acc, e, idx, re, src, aut));
-    if (!aut || m_util.str.is_length(idx)) return;
+    if (!aut || m_util.str.is_length(idx)) {
+        return false;
+    }
     SASSERT(m_autil.is_numeral(idx));
     eautomaton::moves mvs;
     aut->get_moves_from(src, mvs);
@@ -2000,18 +2025,25 @@ void theory_seq::add_accept2step(expr* acc) {
     lits.push_back(~ctx.get_literal(acc));
     if (aut->is_final_state(src)) {
         lits.push_back(mk_literal(m_autil.mk_le(len, idx)));
+        if (ctx.get_assignment(lits.back()) == l_true) {
+            return false;
+        }
     }
     for (unsigned i = 0; i < mvs.size(); ++i) {
         eautomaton::move mv = mvs[i];
         step = mk_step(e, idx, re, src, mv.dst(), mv.t());
         lits.push_back(mk_literal(step));
+        if (ctx.get_assignment(lits.back()) == l_true) {
+            return false;
+        }
     }
     TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
+    //std::cout << lits << "\n";
     for (unsigned i = 0; i < lits.size(); ++i) { // TBD
         ctx.mark_as_relevant(lits[i]);
     }
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-    add_axiom(~ctx.get_literal(acc), mk_literal(m_autil.mk_ge(len, idx)));
+    return false;
 }
 
 
@@ -2019,17 +2051,40 @@ void theory_seq::add_accept2step(expr* acc) {
    acc(s, idx, re, i) & step(s, idx, re, i, j, t) => acc(s, idx + 1, re, j)
 */
 
-void theory_seq::add_step2accept(expr* step) {
+bool theory_seq::add_step2accept(expr* step) {
     context& ctx = get_context();
     SASSERT(ctx.get_assignment(step) == l_true);
-    rational r;
     expr* re, *t, *s, *idx, *i, *j;
     VERIFY(is_step(step, s, idx, re, i, j, t));
-    VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned());    
-    expr_ref idx1(m_autil.mk_int(r.get_unsigned() + 1), m);
     literal acc1 = mk_accept(s, idx,  re, i);
-    literal acc2 = mk_accept(s, idx1, re, j);    
-    add_axiom(~acc1, ~ctx.get_literal(step), acc2);
+    switch (ctx.get_assignment(acc1)) {
+    case l_false:
+        break;
+    case l_undef:
+        return true;
+    case l_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);
+        literal acc2 = mk_accept(s, idx1, re, j);
+        literal_vector lits;
+        lits.push_back(acc1);
+        lits.push_back(ctx.get_literal(step));
+        lits.push_back(~acc2);
+        switch (ctx.get_assignment(acc2)) {
+        case l_undef:
+            propagate_lit(0, 2, lits.c_ptr(), acc2);
+            break;
+        case l_true:
+            break;
+        case l_false:
+            set_conflict(0, lits);
+            break;
+        }
+        break;
+    }
+    }
+    return false;
 }
 
 
@@ -2257,7 +2312,7 @@ bool theory_seq::propagate_automata() {
             reQ = add_reject2reject(e);
         }
         else if (is_step(e)) {
-            add_step2accept(e);
+            reQ = add_step2accept(e);
         }
         else if (m_util.str.is_prefix(e)) {
             reQ = add_prefix2prefix(e);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 92c2ebc05..341c1eb07 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -246,6 +246,30 @@ namespace smt {
             }
         };
 
+        class apply {
+        public:
+            virtual ~apply() {}
+            virtual void operator()(theory_seq& th) = 0;
+        };
+
+        class replay_length_coherence : public apply {
+            expr_ref m_e;
+        public:
+            replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
+            virtual void operator()(theory_seq& th) {
+                th.propagate_length_coherence(m_e);
+            }
+        };
+
+        class push_replay : public trail<theory_seq> {
+            apply* m_apply;
+        public:
+            push_replay(apply* app): m_apply(app) {}
+            virtual void undo(theory_seq& th) {
+                th.m_replay.push_back(m_apply);
+            }
+        };
+
         void erase_index(unsigned idx, unsigned i);
 
         struct stats {
@@ -273,6 +297,7 @@ namespace smt {
         unsigned        m_branch_variable_head;  // index of first equation to examine.
         bool            m_incomplete;            // is the solver (clearly) incomplete for the fragment.
         obj_hashtable<expr> m_length;            // is length applied
+        scoped_ptr_vector<apply> m_replay;       // set of actions to replay
         model_generator* m_mg;
         th_rewriter     m_rewrite;
         seq_util        m_util;
@@ -410,8 +435,8 @@ namespace smt {
         bool is_step(expr* e) const;
         void propagate_step(literal lit, expr* n);
         bool add_reject2reject(expr* rej);
-        void add_accept2step(expr* acc);       
-        void add_step2accept(expr* step);
+        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);