diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 14cfc943f..92d10a81a 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1389,6 +1389,8 @@ namespace smt {
         TRACE(arith, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_bounded_pp(n, m) << "\n";);
         TRACE(bv, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
         if (m.is_bool(n)) {
+            if (!ctx.b_internalized(n))
+                return;
             bool_var v = ctx.get_bool_var(n);
             atom * a   = get_bv2a(v);
             if (a && !a->is_bit()) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 34d30830f..4224a06a4 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1485,8 +1485,7 @@ bool theory_seq::internalize_term(app* term) {
         return true;
     }
     
-    if (m.is_bool(term) && 
-        (m_util.str.is_in_re(term) || m_sk.is_skolem(term))) {
+    if (m.is_bool(term) && (m_util.str.is_in_re(term) || m_sk.is_skolem(term))) {
         bool_var bv = ctx.mk_bool_var(term);
         ctx.set_var_theory(bv, get_id());
         ctx.mark_as_relevant(bv);