diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index a08b58473..15051bf05 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -340,6 +340,8 @@ namespace smt {
     void context::ensure_internalized(expr* e) {
         if (!e_internalized(e)) 
             internalize(e, false);
+        if (is_app(e))
+            internalize_term(to_app(e));
     }
 
     /**
@@ -354,9 +356,8 @@ namespace smt {
 
     void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) {
         internalize_deep(exprs, num_exprs);
-        for (unsigned i = 0; i < num_exprs; ++i) {
+        for (unsigned i = 0; i < num_exprs; ++i) 
             internalize_rec(exprs[i], gate_ctx);
-        }
     }
 
     void context::internalize_rec(expr * n, bool gate_ctx) {
diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index 99d494b72..5c3352ff4 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -161,9 +161,9 @@ namespace smt {
     }
 
     enode* theory::ensure_enode(expr* e) {
-        if (!ctx.e_internalized(e)) {
+        if (!ctx.e_internalized(e)) 
             ctx.internalize(e, is_quantifier(e));
-        }
+        ctx.ensure_internalized(e); // make sure theory variables are attached.
         enode* n = ctx.get_enode(e);
         ctx.mark_as_relevant(n);
         return n;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 76f939936..e04c11d21 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2810,6 +2810,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             f = m_sk.mk_prefix_inv(se1, se2);
             f = mk_concat(se1, f);
             propagate_eq(lit, f, se2, true);
+            propagate_eq(lit, mk_len(f), mk_len(se2), false);
         }
         else {
             propagate_not_prefix(e);
@@ -2823,6 +2824,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             f = m_sk.mk_suffix_inv(se1, se2);
             f = mk_concat(f, se1);
             propagate_eq(lit, f, se2, true);
+            propagate_eq(lit, mk_len(f), mk_len(se2), false);
         }
         else {
             propagate_not_suffix(e);
@@ -2842,6 +2844,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             expr_ref f2 = m_sk.mk_indexof_right(se1, se2);
             f = mk_concat(f1, se2, f2);
             propagate_eq(lit, f, e1, true);
+            propagate_eq(lit, mk_len(f), mk_len(e1), false);
         }
         else {
             propagate_non_empty(lit, se2);