From 5767dfac49f0e94d78f88641862807632c425a0a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 15 Jul 2024 19:39:59 -0700
Subject: [PATCH] fix build of unit test

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/bv_sls_eval.cpp      | 4 ++++
 src/ast/sls/bv_sls_eval.h        | 4 ++--
 src/ast/sls/sls_basic_plugin.cpp | 2 +-
 src/ast/sls/sls_bv_plugin.cpp    | 6 ++----
 src/test/sls_test.cpp            | 4 ++--
 5 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index a53b9b520..4abd4beab 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -634,6 +634,10 @@ namespace bv {
     bool sls_eval::repair_down(app* e, unsigned i) {      
         if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
             ctx.new_value_eh(e->get_arg(i));
+            if (eval_is_correct(e))
+                commit_eval(e);
+            else
+                ctx.new_value_eh(e); // re-queue repair
             return true;
         }
         return false;
diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h
index 0edb4ab5b..02b4104fa 100644
--- a/src/ast/sls/bv_sls_eval.h
+++ b/src/ast/sls/bv_sls_eval.h
@@ -133,6 +133,8 @@ namespace bv {
 
         bool can_eval1(app* e) const;
 
+        void commit_eval(app* e);
+
     public:
         sls_eval(sls_terms& terms, sls::context& ctx);
 
@@ -154,8 +156,6 @@ namespace bv {
         
         sls_valuation& eval(app* e) const;
 
-        void commit_eval(app* e);
-
         void set_random(app* e);
 
         bool eval_is_correct(app* e);
diff --git a/src/ast/sls/sls_basic_plugin.cpp b/src/ast/sls/sls_basic_plugin.cpp
index ef462a9cb..7e571637e 100644
--- a/src/ast/sls/sls_basic_plugin.cpp
+++ b/src/ast/sls/sls_basic_plugin.cpp
@@ -267,7 +267,7 @@ namespace sls {
             if (try_repair(e, j)) 
                 return;            
         }
-        set_value(e, bval1(e));
+        repair_up(e);        
     }
 
     bool basic_plugin::try_repair_distinct(app* e, unsigned i) {
diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
index d958500e2..25c5eea30 100644
--- a/src/ast/sls/sls_bv_plugin.cpp
+++ b/src/ast/sls/sls_bv_plugin.cpp
@@ -100,10 +100,8 @@ namespace sls {
 
     void bv_plugin::repair_down(app* e) {
         unsigned n = e->get_num_args();
-        if (n == 0 || m_eval.eval_is_correct(e)) {
-            m_eval.commit_eval(e);
-            return;
-        }
+        if (n == 0 || m_eval.eval_is_correct(e)) 
+            return;        
 
         if (n == 2) {
             auto d1 = get_depth(e->get_arg(0));
diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp
index 74f5c17df..07888a7e9 100644
--- a/src/test/sls_test.cpp
+++ b/src/test/sls_test.cpp
@@ -178,7 +178,7 @@ namespace bv {
                 auto val2 = ev.bval0(e2);
                 if (val != val2) {
                     ev.set(e2, val);
-                    auto rep1 = ev.try_repair(to_app(e2), idx);
+                    auto rep1 = ev.repair_down(to_app(e2), idx);
                     if (!rep1) {
                         verbose_stream() << "Not repaired " << mk_pp(e1, m) << " " << mk_pp(e2, m) << " r: " << r << "\n";
                     }
@@ -196,7 +196,7 @@ namespace bv {
                 auto& val2 = ev.wval(e2);
                 if (!val1.eq(val2)) {
                     val2.set(val1.bits());
-                    auto rep2 = ev.try_repair(to_app(e2), idx);
+                    auto rep2 = ev.repair_down(to_app(e2), idx);
                     if (!rep2) {
                         verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n";
                     }