From ea44c110bb5c81d4c190c0c601c5aeafa20f2b91 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Dec 2023 20:08:17 -0800
Subject: [PATCH] gc expressions in the scope of updates, not old expressions

---
 src/ast/simplifiers/elim_unconstrained.cpp | 9 +++++++--
 src/sat/smt/euf_solver.cpp                 | 2 +-
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 260f0197426..818800d9947 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -113,7 +113,7 @@ void elim_unconstrained::eliminate() {
 
         IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " / " << rr << " -> " << r << "\n");
         
-        TRACE("elim_unconstrained", tout << mk_pp(t, m) << " -> " << r << "\n");
+        TRACE("elim_unconstrained", tout << mk_pp(t, m) << " / " << rr << " -> " << r << "\n");
         SASSERT(r->get_sort() == t->get_sort());
         m_stats.m_num_eliminated++;
         m_trail.push_back(r);
@@ -271,12 +271,18 @@ void elim_unconstrained::gc(expr* t) {
     while (!todo.empty()) {
         t = todo.back();
         todo.pop_back();
+        
         node& n = get_node(t);  
         if (n.m_refcount == 0)
             continue;
+        if (n.m_term && !is_node(n.m_term))
+            continue;
+
         dec_ref(t);
         if (n.m_refcount != 0)
             continue;
+        if (n.m_term)
+            t = n.m_term;
         if (is_app(t)) {
             for (expr* arg : *to_app(t))
                 todo.push_back(arg);
@@ -436,5 +442,4 @@ void elim_unconstrained::reduce() {
         update_model_trail(*mc, old_fmls);
         mc->reset();
     }
-
 }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index ff11b074938..b108430d8a5 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -1112,7 +1112,7 @@ namespace euf {
             if (b != sat::null_bool_var) {
                 r->m_bool_var2expr.setx(b, n->get_expr(), nullptr);
                 SASSERT(r->m.is_bool(n->get_sort()));
-                IF_VERBOSE(11, verbose_stream() << "set bool_var " << b << " " << r->bpp(n) << " " << mk_bounded_pp(n->get_expr(), m) << "\n");
+                IF_VERBOSE(20, verbose_stream() << "set bool_var " << b << " " << r->bpp(n) << " " << mk_bounded_pp(n->get_expr(), m) << "\n");
             }
         }
         for (auto* s_orig : m_id2solver) {