diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index af0fc6b74..13ba7d67d 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -444,11 +444,12 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
 
     bool found = false;
     for (unsigned i = 0; !found && i < as.size(); ++i) {
-        if (bs.size() > as.size() - i) break;
         all_values &= m().is_value(as[i].get());
-        unsigned j = 0;
-        for (; j < bs.size() && as[j+i].get() == bs[j].get(); ++j) {};
-        found = j == bs.size();
+        if (bs.size() <= as.size() - i) {
+            unsigned j = 0;
+            for (; j < bs.size() && as[j+i].get() == bs[j].get(); ++j) {};
+            found = j == bs.size();
+        }
     }
     if (found) {
         result = m().mk_true();
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index e03cce6c1..40b9fa04b 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2140,13 +2140,13 @@ void theory_seq::deque_axiom(expr* n) {
   lit or s = "" or s = s1*(unit c)
   lit or s = "" or !contains(x*s1, s)
 */
-void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
+void theory_seq::tightest_prefix(expr* s, expr* x) {
     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(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)));
+    add_axiom(s_eq_emp, ~mk_literal(m_util.str.mk_contains(mk_concat(x, s1), s)));
 }
 
 /*
@@ -2160,7 +2160,7 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
 
   len(t) != 0 & !contains(t, s) => i = -1
   len(t) != 0 & contains(t, s) => t = xsy & i = len(x)
-  len(t) != 0 & contains(t, s) & s != emp => tightest_prefix(x, s)
+  tightest_prefix(x, s)
 
   offset not fixed:
 
@@ -2197,7 +2197,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
         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);
+        tightest_prefix(s, x);
     }
     else {
         // offset >= len(t) => indexof(s, t, offset) = -1
@@ -2231,7 +2231,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
 /*
   let r = replace(a, s, t)
 
-  (contains(a, s) -> tightest_prefix(s,xs))
+  tightest_prefix(s, x)
   (contains(a, s) -> r = xty & a = xsy) &
   (!contains(a, s) -> r = a)
 
@@ -2247,7 +2247,7 @@ void theory_seq::add_replace_axiom(expr* r) {
     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);
+    tightest_prefix(s, x);
 }
 
 void theory_seq::add_elim_string_axiom(expr* n) {
@@ -3414,6 +3414,7 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
     VERIFY(m_util.str.is_prefix(e, e1, e2));
     SASSERT(ctx.get_assignment(e) == l_false);
     if (canonizes(false, e)) {
+        TRACE("seq", tout << mk_pp(e, m) << " is false\n";);
         return false;
     }
     expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m);
@@ -3547,11 +3548,13 @@ bool theory_seq::canonizes(bool sign, expr* e) {
     TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";);
     if ((m.is_true(cont) && !sign) ||
         (m.is_false(cont) && sign)) {
+        TRACE("seq", display(tout););
         propagate_lit(deps, 0, 0, ctx.get_literal(e));
         return true;
     }
     if ((m.is_false(cont) && !sign) ||
         (m.is_true(cont) && sign)) {
+        TRACE("seq", display(tout););
         return true;
     }
     return false;
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index f681fbcba..23ab25905 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -443,7 +443,7 @@ namespace smt {
         literal mk_literal(expr* n);
         literal mk_eq_empty(expr* n, bool phase = true);
         literal mk_seq_eq(expr* a, expr* b);
-        void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
+        void tightest_prefix(expr* s, expr* x);
         expr_ref mk_sub(expr* a, expr* b);
         enode* ensure_enode(expr* a);