diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index 47ef73792..38dd4a0e6 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -316,7 +316,7 @@ namespace smt {
     void qi_queue::push_scope() {
         TRACE("new_entries_bug", tout << "[qi:push-scope]\n";);
         m_scopes.push_back(scope());
-        SASSERT(m_new_entries.empty());
+        SASSERT(m_context.inconsistent() || m_new_entries.empty());
         scope & s = m_scopes.back();
         s.m_delayed_entries_lim    = m_delayed_entries.size();
         s.m_instances_lim          = m_instances.size();
@@ -347,6 +347,8 @@ namespace smt {
 
     void qi_queue::init_search_eh() {
         m_subst.reset();
+        m_new_entries.reset();
+        m_delayed_entries.reset();
     }
 
     bool qi_queue::final_check_eh() {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 286141e20..8167d6b40 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3350,7 +3350,7 @@ namespace smt {
         reset_tmp_clauses();
         m_unsat_core.reset();
         m_stats.m_num_checks++;
-        pop_to_base_lvl();
+        pop_to_base_lvl();        
         return true;
     }