From 3c92119b1a9ab3cadc66f7a50bed6cb3f7f8b963 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 24 Aug 2024 09:55:43 -0700
Subject: [PATCH] disable tabu in fallback modes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_arith_base.cpp | 16 ++++------------
 1 file changed, 4 insertions(+), 12 deletions(-)

diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 6f2881cd6..2c537f89c 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -547,18 +547,7 @@ namespace sls {
 
         flet<bool> _tabu(m_use_tabu, false);
         find_reset_moves(lit);
-
-        if (apply_update()) 
-            return true;
-        
-        ++num_fail;
-
-        if (false && num_fail > 3) {
-
-            ctx.force_restart();
-            num_fail = 0;
-        }
-        return false;
+        return apply_update();
     }
 
     template<typename num_t>
@@ -1487,6 +1476,8 @@ namespace sls {
         if (apply_update())
             return eval_is_correct(v);
 
+        flet<bool> _use_tabu(m_use_tabu, false);
+
         m_updates.reset();
         for (auto const& [coeff, w] : coeffs) {
             auto delta = divide(w, sum - old_value, coeff);
@@ -1549,6 +1540,7 @@ namespace sls {
         if (apply_update())
             return eval_is_correct(v);
 
+        flet<bool> _use_tabu(m_use_tabu, false);
         m_updates.reset();
         for (auto [x, p] : monomial)
             add_reset_update(x);