diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp
index 6eb697880..87c146819 100644
--- a/src/qe/qe_sat_tactic.cpp
+++ b/src/qe/qe_sat_tactic.cpp
@@ -631,7 +631,12 @@ namespace qe {
             ctx.set_projection_mode(m_projection_mode_param);
             m_solvers[idx+1]->push();
             while (ctx.get_num_vars() > 0) {
-                VERIFY(l_true == m_solvers[idx+1]->check());
+                lbool r = m_solvers[idx+1]->check();
+                SASSERT(r != l_false);
+                if (r == l_undef) {
+                    checkpoint();
+                    throw tactic_exception("inconclusive solver result");
+                }
                 ctx.project_var(ctx.get_num_vars()-1);               
             }
             m_solvers[idx+1]->pop(1);            
@@ -648,8 +653,8 @@ namespace qe {
             m_Ms[idx] = tmp;
             m_solvers[idx]->assert_expr(not_fml);            
             TRACE("qe", 
-                  tout << mk_pp(fml, m) << "\n--->\n";
-                  tout << mk_pp(tmp, m) << "\n";);
+                  tout << fml << "\n--->\n";
+                  tout << tmp << "\n";);
         }
 
         void checkpoint() {