diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index f30aa90b8..439d60bbf 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -938,7 +938,6 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
 bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
     expr* a, *b;
     zstring s;
- 
     bool lchange = false;
     SASSERT(lhs.empty());
     // solve from back
@@ -1327,6 +1326,13 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex
             found = !rpos.contains(j) && l[i] == r[j];
         }
         if (!found) {
+#if 0
+            std::cout << mk_pp(l[i], m()) << " not found in ";
+            for (unsigned j = 0; j < szr; ++j) {
+                std::cout << mk_pp(r[j], m()) << " ";
+            }
+            std::cout << "\n";
+#endif
             return false;
         }
         SASSERT(0 < j && j <= szr);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 50a32470e..c7fab3934 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1325,7 +1325,10 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
     
     if (concats.size() > 1) {
         for (unsigned i = 0; i < concats.size(); ++i) {
-            sv->add_dependency(ctx.get_enode(concats[i]));
+            expr* e = concats[i];
+            if (!m_util.str.is_string(e)) {
+                sv->add_dependency(ctx.get_enode(e));
+            }
         }
     }
     else if (m_util.str.is_unit(e, e1)) {
@@ -1361,7 +1364,8 @@ app* theory_seq::mk_value(app* e) {
         unsigned sz;
         if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) {
             unsigned v = val.get_unsigned();
-            if ((v < 7) || (14 <= v && v < 32) || v == 127) {
+            if (false && ((v < 7) || (14 <= v && v < 32) || v == 127)) {
+                // disabled: use escape characters.
                 result = m_util.str.mk_unit(result);                
             }
             else {