diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 7342b3c49..d34cad2f4 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -558,6 +558,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_sort(c, a);
         RESET_ERROR_CODE();
+        CHECK_IS_EXPR(a, 0);
         Z3_sort r = of_sort(mk_c(c)->m().get_sort(to_expr(a)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index eccc2d0c7..0e7db9971 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -1491,8 +1491,10 @@ namespace fm {
             unsigned sz = g.size();
             for (unsigned i = 0; i < sz; i++) {
                 expr * f = g[i];
-                if (is_occ(f))
+                if (is_occ(f)) {
+                    TRACE("qe_lite", tout << "OCC: " << mk_ismt2_pp(f, m) << "\n";);
                     continue;
+                }
                 TRACE("qe_lite", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";);
                 quick_for_each_expr(proc, visited, f);
             }
@@ -2221,6 +2223,9 @@ namespace fm {
         void operator()(expr_ref_vector& fmls) {
             init(fmls);
             init_use_list(fmls);
+            for (auto & f : fmls) {
+                if (has_quantifiers(f)) return;
+            }
             if (m_inconsistent) {
                 m_new_fmls.reset();
                 m_new_fmls.push_back(m.mk_false());
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index c98040c17..3b70e1426 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2180,8 +2180,12 @@ void theory_seq::internalize_eq_eh(app * atom, bool_var v) {
 }
 
 bool theory_seq::internalize_atom(app* a, bool) {
-    return internalize_term(a);
 #if 0
+    return internalize_term(a);
+#else
+    if (is_skolem(m_eq, a)) {
+        return internalize_term(a);
+    }
     context & ctx   = get_context();
     bool_var bv = ctx.mk_bool_var(a);
     ctx.set_var_theory(bv, get_id());
@@ -2196,7 +2200,7 @@ bool theory_seq::internalize_atom(app* a, bool) {
         m_util.str.is_suffix(a, e1, e2)) {
         return internalize_term(to_app(e1)) && internalize_term(to_app(e2));        
     }
-    if (is_accept(a) || is_reject(a) || is_skolem(m_eq, a) || is_step(a) || is_skolem(symbol("seq.is_digit"), a)) {
+    if (is_accept(a) || is_reject(a) || is_step(a) || is_skolem(symbol("seq.is_digit"), a)) {
         return true;
     }
     UNREACHABLE();