diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index c85d15378..2b4dc05dd 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3512,6 +3512,7 @@ namespace smt {
         TRACE("after_search", display(tout << "result: " << r << "\n");
               m_case_split_queue->display(tout << "case splits\n");
               );
+        m_search_finalized = true;
         display_profile(verbose_stream());
         if (r == l_true && get_cancel_flag()) 
             r = l_undef;
@@ -3638,6 +3639,7 @@ namespace smt {
             return check(0, nullptr, reset_cancel);
         }
         else {
+            search_completion sc(*this);
             TRACE("before_search", display(tout););
             return check_finalize(search());
         }
@@ -3685,6 +3687,7 @@ namespace smt {
         if (!check_preamble(reset_cancel)) return l_undef;
         SASSERT(at_base_level());
         setup_context(false);
+        search_completion sc(*this);
         if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {            
             expr_ref_vector asms(m, num_assumptions, assumptions);
             parallel p(*this);
@@ -3716,6 +3719,7 @@ namespace smt {
         TRACE("before_search", display(tout););
         setup_context(false);
         lbool r = l_undef;
+        search_completion sc(*this);
         do {
             pop_to_base_lvl();
             expr_ref_vector asms(cube);
@@ -4728,12 +4732,14 @@ namespace smt {
     }
 
     void context::get_model(model_ref & mdl) {
-        if (inconsistent()) 
+        if (inconsistent())
             mdl = nullptr;
-        else if (m_model.get()) 
+        else if (m_model.get())
             mdl = m_model.get();
         else if (!m.inc())
             mdl = nullptr;
+        else if (!m_search_finalized)
+            mdl = nullptr;
         else {
             mk_proto_model();
             if (!m_model && m_proto_model) {
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index a7b3ce124..d44da1e87 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1575,6 +1575,13 @@ namespace smt {
         bool already_internalized_theory_core(theory * th, expr_ref_vector const & s) const;
 #endif
         bool check_preamble(bool reset_cancel);
+
+        struct search_completion {
+            context& ctx;
+            search_completion(context& ctx) : ctx(ctx) { ctx.m_search_finalized = false; }
+            ~search_completion() { if (!ctx.m_search_finalized) ctx.m_last_search_failure = CANCELED; }
+        };
+        bool m_search_finalized = true;
         lbool check_finalize(lbool r);
 
         // -----------------------------------
diff --git a/src/smt/smt_failure.h b/src/smt/smt_failure.h
index ab706297f..15890dd5b 100644
--- a/src/smt/smt_failure.h
+++ b/src/smt/smt_failure.h
@@ -30,7 +30,7 @@ namespace smt {
         CANCELED,      //!< External cancel flag was set
         NUM_CONFLICTS, //!< Maximum number of conflicts was reached
         THEORY,        //!< Theory is incomplete
-        RESOURCE_LIMIT,
+        RESOURCE_LIMIT,       
         LAMBDAS,       //!< Logical context contains lambdas.
         QUANTIFIERS    //!< Logical context contains universal quantifiers.
     };