diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 3a2aacd26..623141038 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -419,6 +419,7 @@ namespace smt {
         visitor.collect(fmls);
         visitor.display_decls(out);
         visitor.display_asserts(out, fmls, true);
+        out << "(check-sat)\n";
     }
 
     static unsigned g_lemma_id = 0;
@@ -464,6 +465,7 @@ namespace smt {
         visitor.collect(fmls);
         visitor.display_decls(out);
         visitor.display_asserts(out, fmls, true);
+        out << "(check-sat)\n";
     }
 
     void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index b1ca67274..a4930b357 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -104,7 +104,18 @@ namespace nra {
             }
             // TBD: add variable bounds?
 
-            lbool r = m_nlsat->check(); 
+            lbool r = l_undef;
+            try {
+                r = m_nlsat->check(); 
+            }
+            catch (z3_exception&) {
+                if (m_limit.get_cancel_flag()) {
+                    r = l_undef;
+                }
+                else {
+                    throw;
+                }
+            }
             TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n"););
             switch (r) {
             case l_true: