From 93086143b3f5de25278b8aefef1b41ece32c83d1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 21 Oct 2024 19:57:47 -0700
Subject: [PATCH] fix dirty flag setting

---
 src/ast/simplifiers/elim_unconstrained.cpp | 13 +++++++------
 src/ast/sls/sls_bv_plugin.cpp              |  4 +++-
 src/sat/smt/sls_solver.cpp                 | 18 ++++++++++--------
 3 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 818800d99..a355f823a 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -80,13 +80,13 @@ void elim_unconstrained::eliminate() {
             continue;
         }
         expr* e = get_parent(v);
-        IF_VERBOSE(11, for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";);
+        TRACE("elim_unconstrained", for (expr* p : n.m_parents) tout << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";);
         if (!e || !is_app(e) || !is_ground(e)) {
             n.m_refcount = 0;
             continue;
         }
         if (m_heap.contains(root(e))) {
-            IF_VERBOSE(11, verbose_stream() << "already in heap " << mk_bounded_pp(e, m) << "\n");
+            TRACE("elim_unconstrained", tout << "already in heap " << mk_bounded_pp(e, m) << "\n");
             continue;
         }
         app* t = to_app(e);
@@ -107,7 +107,7 @@ void elim_unconstrained::eliminate() {
         n.m_refcount = 0;
         m_args.shrink(sz);
         if (!inverted) {
-            IF_VERBOSE(11, verbose_stream() << "not inverted " << mk_bounded_pp(e, m) << "\n");
+            TRACE("elim_unconstrained", tout << "not inverted " << mk_bounded_pp(e, m) << "\n");
             continue;
         }
 
@@ -147,10 +147,10 @@ expr* elim_unconstrained::get_parent(unsigned n) const {
 }
 
 void elim_unconstrained::invalidate_parents(expr* e) {
-    ptr_vector<expr> todo;
+    ptr_buffer<expr> todo;
     do {
         node& n = get_node(e);
-        if (!n.m_dirty) {
+        if (!n.m_dirty && e == n.m_term) {
             n.m_dirty = true;
             for (expr* e : n.m_parents)
                 todo.push_back(e);            
@@ -299,7 +299,7 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
         return expr_ref(t, m);
     if (!is_node(t))
         return expr_ref(t, m);
-    ptr_vector<expr> todo;
+    ptr_buffer<expr> todo;
     todo.push_back(t);
     while (!todo.empty()) {
         t = todo.back();
@@ -310,6 +310,7 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
         unsigned sz0 = todo.size();
         if (is_app(t)) {     
             if (n.m_term != t) {
+                n.m_dirty = false;
                 todo.pop_back();
                 continue;
             }
diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
index 14a2d1758..8b4b29be7 100644
--- a/src/ast/sls/sls_bv_plugin.cpp
+++ b/src/ast/sls/sls_bv_plugin.cpp
@@ -57,8 +57,10 @@ namespace sls {
             return;
         auto a = to_app(e);
 
-        if (!m_eval.eval_is_correct(a))
+        if (!m_eval.eval_is_correct(a)) {
+            IF_VERBOSE(20, verbose_stream() << "repair " << lit << " " << mk_bounded_pp(e, m) << "\n");
             ctx.new_value_eh(e);
+        }
     }
 
     bool bv_plugin::propagate() {
diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp
index cfdf30c64..f5217db17 100644
--- a/src/sat/smt/sls_solver.cpp
+++ b/src/sat/smt/sls_solver.cpp
@@ -234,18 +234,20 @@ namespace sls {
         }
 
         void export_phase_to_smt() {
-            if (m_has_new_sls_phase) {
-                IF_VERBOSE(1, verbose_stream() << "new SLS -> SMT phase\n");
-                std::lock_guard<std::mutex> lock(s.m_mutex);
-                for (unsigned i = 0; i < m_sls_phase.size(); ++i)
-                    s.s().set_phase(sat::literal(i, !m_sls_phase[i]));
-                m_has_new_sls_phase = false;
-            }
+            if (!m_has_new_sls_phase)
+                return;
+            IF_VERBOSE(1, verbose_stream() << "new SLS -> SMT phase\n");
+            std::lock_guard<std::mutex> lock(s.m_mutex);
+            for (unsigned i = 0; i < m_sls_phase.size(); ++i)
+                s.s().set_phase(sat::literal(i, !m_sls_phase[i]));
+            m_has_new_sls_phase = false;
         }
 
         void import_phase_from_smt() {
-            IF_VERBOSE(1, verbose_stream() << "new SMT -> SLS phase\n");
+            if (m_has_new_sat_phase)
+                return;
             m_has_new_sat_phase = true;
+            IF_VERBOSE(1, verbose_stream() << "new SMT -> SLS phase\n");
             s.s().set_has_new_best_phase(false);
             std::lock_guard<std::mutex> lock(s.m_mutex);
             for (auto v : m_shared_vars)