diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index eb764698c..f6d81bec1 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -95,7 +95,7 @@ namespace smt {
     // -----------------------------------------------------------------------
 
     bool theory_nseq::internalize_atom(app* atom, bool /*gate_ctx*/) {
-        // std::cout << "internalize_atom: " << mk_pp(atom, m) << std::endl;
+        std::cout << "internalize_atom: " << mk_pp(atom, m) << std::endl;
         // str.in_re atoms are boolean predicates: register as bool_var
         // so that assign_eh fires when the SAT solver assigns them.
         // Following theory_seq: create a bool_var directly without an enode
@@ -127,7 +127,7 @@ namespace smt {
     }
 
     bool theory_nseq::internalize_term(app* term) {
-        // std::cout << "internalize_term: " << mk_pp(term, m) << std::endl;
+        std::cout << "internalize_term: " << mk_pp(term, m) << std::endl;
         // ensure ALL children are internalized (following theory_seq pattern)
         for (auto arg : *term) {
             mk_var(ensure_enode(arg));
diff --git a/src/smt/theory_seq_len.cpp b/src/smt/theory_seq_len.cpp
index 4eb50fd7b..5c7ace437 100644
--- a/src/smt/theory_seq_len.cpp
+++ b/src/smt/theory_seq_len.cpp
@@ -47,6 +47,13 @@ namespace smt {
             mk_var(ctx.get_enode(s));
             return true;
         }
+        if (m_util.is_skolem(atom)) {
+            // char2bit
+            bool_var bv = ctx.mk_bool_var(atom);
+            ctx.set_var_theory(bv, get_id());
+            ctx.mark_as_relevant(bv);
+            return true;
+    }
         return internalize_term(atom);
     }