diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 61488638c..fc9a7f3d5 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -139,6 +139,7 @@ void theory_str::assert_implication(expr * premise, expr * conclusion) {
 }
 
 bool theory_str::internalize_atom(app * atom, bool gate_ctx) {
+    /*
     TRACE("t_str", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << std::endl;);
     SASSERT(atom->get_family_id() == get_family_id());
 
@@ -152,15 +153,21 @@ bool theory_str::internalize_atom(app * atom, bool gate_ctx) {
         ctx.internalize(atom->get_arg(i), false);
 
     literal l(ctx.mk_bool_var(atom));
+
     ctx.set_var_theory(l.var(), get_id());
 
     return true;
+    */
+    return internalize_term(atom);
 }
 
 bool theory_str::internalize_term(app * term) {
     context & ctx = get_context();
+    ast_manager & m = get_manager();
     TRACE("t_str", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << std::endl;);
     SASSERT(term->get_family_id() == get_family_id());
+
+    /* // what I had before
     SASSERT(!ctx.e_internalized(term));
 
     unsigned num_args = term->get_num_args();
@@ -175,15 +182,67 @@ bool theory_str::internalize_term(app * term) {
 
     attach_new_th_var(e);
 
-    /*
-    if (is_concat(term)) {
-        instantiate_concat_axiom(e);
-    }
+    //if (is_concat(term)) {
+    //    instantiate_concat_axiom(e);
+    //}
     */
 
+    // from theory_seq::internalize_term()
+    if (ctx.e_internalized(term)) {
+        enode* e = ctx.get_enode(term);
+        mk_var(e);
+        return true;
+    }
+    unsigned num_args = term->get_num_args();
+    expr* arg;
+    for (unsigned i = 0; i < num_args; i++) {
+        arg = term->get_arg(i);
+        mk_var(ensure_enode(arg));
+    }
+    if (m.is_bool(term)) {
+        bool_var bv = ctx.mk_bool_var(term);
+        ctx.set_var_theory(bv, get_id());
+        ctx.mark_as_relevant(bv);
+    }
+
+    enode* e = 0;
+    if (ctx.e_internalized(term)) {
+        e = ctx.get_enode(term);
+    }
+    else {
+        e = ctx.mk_enode(term, false, m.is_bool(term), true);
+    }
+    mk_var(e);
+
     return true;
 }
 
+enode* theory_str::ensure_enode(expr* e) {
+    context& ctx = get_context();
+    if (!ctx.e_internalized(e)) {
+        ctx.internalize(e, false);
+    }
+    enode* n = ctx.get_enode(e);
+    ctx.mark_as_relevant(n);
+    return n;
+}
+
+theory_var theory_str::mk_var(enode* n) {
+    if (!m_strutil.is_string(n->get_owner())) {
+        return null_theory_var;
+    }
+    if (is_attached_to_var(n)) {
+        return n->get_th_var(get_id());
+    }
+    else {
+        theory_var v = theory::mk_var(n);
+        // m_find.mk_var();
+        get_context().attach_th_var(n, this, v);
+        get_context().mark_as_relevant(n);
+        return v;
+    }
+}
+
 static void cut_vars_map_copy(std::map<expr*, int> & dest, std::map<expr*, int> & src) {
     std::map<expr*, int>::iterator itor = src.begin();
     for (; itor != src.end(); itor++) {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index ca985cb8f..af2ea1db6 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -208,6 +208,8 @@ namespace smt {
     protected:
         virtual bool internalize_atom(app * atom, bool gate_ctx);
         virtual bool internalize_term(app * term);
+        virtual enode* ensure_enode(expr* e);
+        virtual theory_var mk_var(enode * n);
 
         virtual void new_eq_eh(theory_var, theory_var);
         virtual void new_diseq_eh(theory_var, theory_var);
@@ -224,7 +226,7 @@ namespace smt {
         virtual void propagate();
 
         virtual final_check_status final_check_eh();
-        void attach_new_th_var(enode * n);
+        virtual void attach_new_th_var(enode * n);
 
         virtual void init_model(model_generator & m);
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);