diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 2e102f4e4..624a5dfcf 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1761,7 +1761,7 @@ namespace qe {
             // unless the current state is unsatisfiable.
             // 
             if (m.is_true(fml_mixed)) {
-                SASSERT(l_true == m_solver.check());
+                SASSERT(l_false != m_solver.check());
                 m_current = m_current->add_child(fml_closed);
                 for (unsigned i = 0; m_defs && i < m_current->num_free_vars(); ++i) {
                     expr_ref val(m);
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index d78ccbe9b..fb151d78e 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -22,6 +22,7 @@ Notes:
 
 #include "ast/expr_abstract.h"
 #include "ast/ast_util.h"
+#include "ast/occurs.h"
 #include "ast/rewriter/quant_hoist.h"
 #include "ast/ast_pp.h"
 #include "ast/rewriter/th_rewriter.h"
@@ -919,9 +920,6 @@ namespace qe {
             if (level.max() == UINT_MAX) {
                 num_scopes = 2*(m_level/2);
             }
-            else if (m_mode == qsat_qe_rec) {
-                num_scopes = 2;
-            }
             else {
                 if (level.max() + 2 > m_level) return false;
                 SASSERT(level.max() + 2 <= m_level);
@@ -1016,11 +1014,16 @@ namespace qe {
                     
                     TRACE("qe", tout << "elim-rec " << tmp << "\n";);
                     tmp = elim(vars, tmp);
+                    if (!tmp) {
+                        visited.insert(e, e);
+                        todo.pop_back();
+                        break;
+                    }
                     if (is_fa) {
                         tmp = ::push_not(tmp);
                     }
                     trail.push_back(tmp);
-                    TRACE("qe", tout << vars << ": " << tmp << "\n";);
+                    TRACE("qe", tout << tmp << "\n";);
                     visited.insert(e, tmp);
                     todo.pop_back();
                     break;
@@ -1037,14 +1040,12 @@ namespace qe {
         /*
          * Solve ex (x) phi(x)
          */
-        expr_ref elim(app_ref_vector const& vars, expr* _fml) {
-            expr_ref save(_fml, m);
+        expr_ref elim(app_ref_vector& vars, expr* _fml) {
             expr_ref fml(_fml, m);
             expr_ref_vector defs(m);
             if (has_quantifiers(fml)) {
-                return fml; 
+                return expr_ref(m);
             }
-            flet<qsat_mode> _mode(m_mode, qsat_qe);
             reset();
             fml = ::mk_exists(m, vars.size(), vars.c_ptr(), fml);
             fml = ::push_not(fml);
@@ -1061,12 +1062,20 @@ namespace qe {
             TRACE("qe", tout << "ex: " << fml << "\n";);
             lbool is_sat = check_sat();
             
+            unsigned j = 0;
             switch (is_sat) {
             case l_false:
                 fml = ::mk_and(m_answer);
+                for (app* v : m_free_vars) {
+                    if (occurs(v, fml)) m_free_vars[j++] = v;
+                }
+                m_free_vars.shrink(j);
+                if (!m_free_vars.empty()) {
+                    fml = ::mk_exists(m, m_free_vars.size(), m_free_vars.c_ptr(), fml);
+                }
                 return fml;
             default:
-                return save;
+                return expr_ref(m);
             }
         }