diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 6fff9aff4..4d55632d3 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -595,6 +595,9 @@ void rewriter_tpl<Config>::set_inv_bindings(unsigned num_bindings, expr * const
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
+    if (m().canceled()) {
+        throw rewriter_exception(m().limit().get_cancel_msg());
+    }
     SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
     SASSERT(not_rewriting());
     m_root      = t;
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index 50814b686..6b626c2de 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -420,14 +420,14 @@ namespace smt {
             case l_undef:
                 break;
             case l_true:
-                m_proto_model->eval(n, res, false);
+                if (!m_proto_model->eval(n, res, false)) return true;
                 CTRACE("mbqi_bug", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); 
                 if (m.is_false(res)) {
                     return false;
                 }
                 break;
             case l_false:
-                m_proto_model->eval(n, res, false);
+                if (!m_proto_model->eval(n, res, false)) return true;
                 CTRACE("mbqi_bug", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); 
                 if (m.is_true(res)) {
                     return false;
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index a425475c2..f166125ba 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -149,6 +149,7 @@ namespace smt {
                     SASSERT(!contains_model_value(t));
                     unsigned gen = (*it).m_value;
                     expr * t_val = ev.eval(t, true);
+                    if (!t_val) break;
                     TRACE("model_finder", tout << mk_pp(t, m_manager) << " " << mk_pp(t_val, m_manager) << "\n";);
 
                     expr * old_t = 0;
@@ -828,7 +829,7 @@ namespace smt {
                 for (; it != end; ++it) {
                     expr *     t = (*it).m_key;
                     expr * t_val = eval(t, true);
-                    if (!already_found.contains(t_val)) {
+                    if (t_val && !already_found.contains(t_val)) {
                         values.push_back(t_val);
                         already_found.insert(t_val);
                     }
@@ -891,6 +892,7 @@ namespace smt {
                 add_mono_exceptions(n);
                 ptr_buffer<expr> values;
                 get_instantiation_set_values(n, values);
+                if (values.empty()) return;
                 sort_values(n, values);
                 sort * s = n->get_sort();
                 arith_simplifier_plugin * as = get_arith_simp();