diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 3bc902ddd..2fa79b2ce 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -616,7 +616,6 @@ struct model_evaluator::imp : public rewriter_tpl<mev::evaluator_cfg> {
                                     false, // no proofs for evaluator
                                     m_cfg),
         m_cfg(md.get_manager(), md, p) {
-        set_cancel_check(false);
     }
     void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
     void reset() {
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 7b0877c62..e0214972b 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -162,13 +162,13 @@ namespace smt {
        The variables are replaced by skolem constants. These constants are stored in sks.
     */
 
-    void model_checker::assert_neg_q_m(quantifier * q, expr_ref_vector & sks) {
+    bool model_checker::assert_neg_q_m(quantifier * q, expr_ref_vector & sks) {
         expr_ref tmp(m);
         
         TRACE("model_checker", tout << "curr_model:\n"; model_pp(tout, *m_curr_model););
 
         if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
-            return;
+            return false;
         }
         TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
         ptr_buffer<expr> subst_args;
@@ -191,6 +191,7 @@ namespace smt {
         r = m.mk_not(sk_body);
         TRACE("model_checker", tout << "mk_neg_q_m:\n" << mk_ismt2_pp(r, m) << "\n";);
         m_aux_context->assert_expr(r);
+        return true;
     }
 
     bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
@@ -333,7 +334,8 @@ namespace smt {
         TRACE("model_checker", tout << "model checking:\n" << expr_ref(flat_q->get_expr(), m) << "\n";);
         expr_ref_vector sks(m);
 
-        assert_neg_q_m(flat_q, sks);
+        if (!assert_neg_q_m(flat_q, sks))
+            return false;
         TRACE("model_checker", tout << "skolems:\n" << sks << "\n";);
 
         flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index c6006bcb3..6332a890e 100644
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@@ -62,7 +62,7 @@ namespace smt {
         expr * get_type_compatible_term(expr * val);
         expr_ref replace_value_from_ctx(expr * e);
         void restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe);
-        void assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
+        bool assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
         bool add_blocking_clause(model * cex, expr_ref_vector & sks);
         bool check(quantifier * q);
         void check_quantifiers(bool& found_relevant, unsigned& num_failures);