From cd331b8a56bfb76208c0e27e8daef6e2db2a4694 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 22 Dec 2023 13:17:04 -0800
Subject: [PATCH] remove reference to tactic.h

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/bvsls_opt_engine.cpp |  6 ++++--
 src/ast/sls/sls_engine.cpp       | 13 ++++++-------
 src/ast/sls/sls_engine.h         |  1 -
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/ast/sls/bvsls_opt_engine.cpp b/src/ast/sls/bvsls_opt_engine.cpp
index e4c96d735bd..7dc71cd8cdf 100644
--- a/src/ast/sls/bvsls_opt_engine.cpp
+++ b/src/ast/sls/bvsls_opt_engine.cpp
@@ -68,7 +68,8 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
 
         if (is_sat != l_true) {
             do {
-                checkpoint();
+                if (!m_manager.inc())
+                    return res;
 
                 IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
                 is_sat = search();
@@ -136,7 +137,8 @@ expr_ref bvsls_opt_engine::maximize()
 
     while (m_mpz_manager.lt(score, max_score) && check_restart(m_stats.m_moves))
     {
-        checkpoint();
+        if (!m_manager.inc())
+            goto bailout;
         m_stats.m_moves++;
         m_mpz_manager.set(old_score, score);
         new_const = (unsigned)-1;
diff --git a/src/ast/sls/sls_engine.cpp b/src/ast/sls/sls_engine.cpp
index 8b425374779..8bf70f3dd24 100644
--- a/src/ast/sls/sls_engine.cpp
+++ b/src/ast/sls/sls_engine.cpp
@@ -23,7 +23,6 @@ Module Name:
 #include "ast/ast_pp.h"
 #include "ast/rewriter/var_subst.h"
 #include "model/model_pp.h"
-#include "tactic/tactic.h"
 #include "util/luby.h"
 
 #include "params/sls_params.hpp"
@@ -91,14 +90,12 @@ void sls_engine::collect_statistics(statistics& st) const {
     st.update("sls moves/sec", m_stats.m_moves / seconds);
 }
 
-void sls_engine::checkpoint() {
-    tactic::checkpoint(m_manager);
-}
 
 bool sls_engine::full_eval(model & mdl) {
     model::scoped_model_completion _scm(mdl, true);
     for (expr* a : m_assertions) {
-        checkpoint();        
+        if (!m_manager.inc())
+            return false;
         if (!mdl.is_true(a)) {
             TRACE("sls", tout << "Evaluation: false\n";);
             return false;
@@ -422,7 +419,8 @@ lbool sls_engine::search() {
     unsigned sz = m_assertions.size();
 
     while (check_restart(m_stats.m_moves)) {
-        checkpoint();
+        if (!m_manager.inc())
+            return l_undef;
         m_stats.m_moves++;
 
         // Andreas: Every base restart interval ...
@@ -532,7 +530,8 @@ lbool sls_engine::operator()() {
     lbool res = l_undef;
 
     do {
-        checkpoint();
+        if (!m_manager.inc())
+            return l_undef;
 
         // report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
         res = search();
diff --git a/src/ast/sls/sls_engine.h b/src/ast/sls/sls_engine.h
index 88ebb98b8cd..32338b8ae83 100644
--- a/src/ast/sls/sls_engine.h
+++ b/src/ast/sls/sls_engine.h
@@ -117,7 +117,6 @@ class sls_engine {
     unsynch_mpz_manager& get_mpz_manager() { return m_mpz_manager; }
 
 protected:
-    void checkpoint();
 
     bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
                  double & best_score, unsigned & best_const, mpz & best_value);