diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 13ca17764..d923014c1 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -141,6 +141,7 @@ namespace sat {
         m_participated.reset();
         m_canceled.reset();
         m_reasoned.reset();
+        m_case_split_queue.reset();
         m_simplifier.reset_todos();
         m_qhead = 0;
         m_trail.reset();
@@ -3541,7 +3542,7 @@ namespace sat {
             else {
                 set_eliminated(v, true);
                 if (!is_external(v) || true) {
-                    m_free_vars.push_back(v);
+                    m_free_vars.push_back(v);                   
                 }
             }
         }
@@ -3556,6 +3557,7 @@ namespace sat {
             bool_var v = m_free_vars[i];
             cleanup_watch(literal(v, false));
             cleanup_watch(literal(v, true));
+            
         }
         TRACE("sat",
             tout << "clauses to reinit: " << (m_clauses_to_reinit.size() - old_sz) << "\n";
@@ -3574,10 +3576,10 @@ namespace sat {
                 m_free_vars[j++] = w;
         m_free_vars.shrink(j);
 
-        for (bool_var i = v; i < m_justification.size(); ++i) {
-            m_case_split_queue.del_var_eh(i);
-            m_probing.reset_cache(literal(i, true));
-            m_probing.reset_cache(literal(i, false));
+        for (bool_var w = m_justification.size(); w-- > v;) {
+            m_case_split_queue.del_var_eh(w);
+            m_probing.reset_cache(literal(w, true));
+            m_probing.reset_cache(literal(w, false));
         }
         m_watches.shrink(2*v);
         m_assignment.shrink(2*v);
@@ -3600,6 +3602,7 @@ namespace sat {
     void solver::pop(unsigned num_scopes) {
         if (num_scopes == 0)
             return;
+        unsigned free_vars_head = m_free_vars.size();
         if (m_ext) {
             pop_vars(num_scopes);
             m_ext->pop(num_scopes);
@@ -3609,6 +3612,8 @@ namespace sat {
         scope & s        = m_scopes[new_lvl];
         m_inconsistent   = false; // TBD: use model seems to make this redundant: s.m_inconsistent;
         unassign_vars(s.m_trail_lim, new_lvl);
+        for (unsigned i = m_free_vars.size(); i-- > free_vars_head; )
+            m_case_split_queue.del_var_eh(m_free_vars[i]);
         m_scope_lvl -= num_scopes;
         reinit_clauses(s.m_clauses_to_reinit_lim);
         m_scopes.shrink(new_lvl);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index f22ef3aec..7999676d6 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -1057,7 +1057,7 @@ private:
             CTRACE("sat", !m.is_true(tmp),
                    tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
                    model_smt2_pp(tout, m, *(mdl.get()), 0););
-            if (!m.is_true(tmp)) {
+            if (m.is_false(tmp)) {
                 IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n");
                 IF_VERBOSE(0, verbose_stream() << "evaluated to " << tmp << "\n");
                 all_true = false;
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 529d169b7..658bdb8e3 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -8,7 +8,7 @@ Module Name:
 Abstract:
 
     E-matching quantifier instantiation plugin
-
+    
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-01-24
@@ -374,6 +374,7 @@ namespace q {
         clause* cl = alloc(clause, m, m_clauses.size());
         cl->m_literal = ctx.mk_literal(_q);
         quantifier_ref q(_q, m);
+        q = m_qs.flatten(q);
         if (is_exists(q)) {
             cl->m_literal.neg();
             expr_ref body(mk_not(m, q->get_expr()), m);
diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp
index 8f03d4d8b..c1d22ad36 100644
--- a/src/sat/smt/q_eval.cpp
+++ b/src/sat/smt/q_eval.cpp
@@ -157,6 +157,7 @@ namespace q {
             expr* t = todo.back();
             SASSERT(!is_ground(t) || ctx.get_egraph().find(t));
             if (is_ground(t)) {
+                m_mark.mark(t);
                 m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);
                 SASSERT(m_eval[t->get_id()]);
                 todo.pop_back();