diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 087f02440..7f479c7ef 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -104,6 +104,8 @@ namespace smt {
     */
 
     bool context::get_cancel_flag() {
+        if (l_true == m_sls_completed)
+            return true;
         if (m.limit().inc())
             return false;
         m_last_search_failure = CANCELED;
@@ -3507,10 +3509,11 @@ namespace smt {
         if (r == l_true && get_cancel_flag()) {
             r = l_undef;
         }
-        if (r == l_undef && get_cancel_flag() && has_sls_model()) {
+        if (r == l_undef && m_sls_completed == l_true && has_sls_model()) {
             m.limit().reset_cancel();
             r = l_true;
         }
+        m_sls_completed = l_false;
         if (r == l_true && gparams::get_value("model_validate") == "true") {
             recfun::util u(m);
             if (u.get_rec_funs().empty() && m_proto_model) {
@@ -3750,6 +3753,7 @@ namespace smt {
         m_phase_default                = false;
         m_case_split_queue             ->init_search_eh();
         m_next_progress_sample         = 0;
+        m_sls_completed                = l_undef;
         if (m.has_type_vars() && !m_theories.get_plugin(poly_family_id))
             register_plugin(alloc(theory_polymorphism, *this));
         TRACE("literal_occ", display_literal_num_occs(tout););
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index fe2bc0f6f..2558653ce 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -128,6 +128,7 @@ namespace smt {
         class parallel*             m_par = nullptr;
         unsigned                    m_par_index = 0;
         bool                        m_internalizing_assertions = false;
+        lbool                       m_sls_completed = l_undef;
 
 
         // -----------------------------------
@@ -288,6 +289,11 @@ namespace smt {
 
         bool get_cancel_flag();
 
+        void set_sls_completed() {
+            if (m_sls_completed == l_undef)
+                m_sls_completed = l_true;
+        }
+
         region & get_region() {
             return m_region;
         }
diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp
index 2caccee49..4795620d7 100644
--- a/src/smt/theory_sls.cpp
+++ b/src/smt/theory_sls.cpp
@@ -58,7 +58,7 @@ namespace smt {
     }
     
     void theory_sls::set_finished() {
-        m.limit().cancel();
+        ctx.set_sls_completed();     
     }
     
     unsigned theory_sls::get_num_bool_vars() const {