From 7699ce56dbabaa91a11d0fb18209966860e209eb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Aug 2024 10:39:15 -0700
Subject: [PATCH] fixing repair

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_bv_plugin.cpp | 21 ++++++++++++++-------
 src/ast/sls/sls_bv_plugin.h   |  1 +
 src/ast/sls/sls_context.cpp   |  2 ++
 3 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
index 1f3be03e9..dea6ece87 100644
--- a/src/ast/sls/sls_bv_plugin.cpp
+++ b/src/ast/sls/sls_bv_plugin.cpp
@@ -39,13 +39,19 @@ namespace sls {
         return expr_ref(bv.mk_numeral(val.get_value(), e->get_sort()), m);
     }
 
+    bool bv_plugin::is_bv_predicate(expr* e) {
+        return e && is_app(e) && to_app(e)->get_family_id() == bv.get_family_id();
+    }
+
     void bv_plugin::propagate_literal(sat::literal lit) {       
         SASSERT(ctx.is_true(lit));
-        auto a = ctx.atom(lit.var());
-        if (!a || !is_app(a))
+        auto e = ctx.atom(lit.var());
+        if (!is_bv_predicate(e))
             return;
-        if (!m_eval.eval_is_correct(to_app(a)))
-            ctx.new_value_eh(a);
+        auto a = to_app(e);
+
+        if (!m_eval.eval_is_correct(a))
+            ctx.new_value_eh(e);
     }
 
     bool bv_plugin::propagate() {
@@ -145,10 +151,11 @@ namespace sls {
 
     void bv_plugin::repair_literal(sat::literal lit) {
         SASSERT(ctx.is_true(lit));
-        auto a = ctx.atom(lit.var());
-        if (!a || !is_app(a))
+        auto e = ctx.atom(lit.var());
+        if (!is_bv_predicate(e))
             return;
-        if (!m_eval.eval_is_correct(to_app(a)))
+        auto a = to_app(e);
+        if (!m_eval.eval_is_correct(a))
             ctx.flip(lit.var());
     }
 
diff --git a/src/ast/sls/sls_bv_plugin.h b/src/ast/sls/sls_bv_plugin.h
index 9cee67ac4..a8fa08dd0 100644
--- a/src/ast/sls/sls_bv_plugin.h
+++ b/src/ast/sls/sls_bv_plugin.h
@@ -34,6 +34,7 @@ namespace sls {
         std::ostream& trace_repair(bool down, expr* e);
         void trace();
         bool can_propagate();
+        bool is_bv_predicate(expr* e);
 
     public:
         bv_plugin(context& ctx);
diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index 62c206812..e04db76f1 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -401,6 +401,7 @@ namespace sls {
         auto is_visited = [&](expr* e) {
             return nullptr != m_allterms.get(e->get_id(), nullptr);
         };
+        
         auto visit = [&](expr* e) {
             m_allterms.setx(e->get_id(), e);
         };
@@ -451,6 +452,7 @@ namespace sls {
 
         m_repair_down.reserve(e->get_id() + 1);
         m_repair_up.reserve(e->get_id() + 1);
+        SASSERT(e == term(e->get_id()));
         if (!m_repair_down.contains(e->get_id()))
             m_repair_down.insert(e->get_id());
         for (auto p : parents(e)) {