gc expressions in the scope of updates, not old expressions

Z3Prover · Dec 19, 2023 · ea44c11 · ea44c11
1 parent 842385a
commit ea44c11
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git 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
@@ -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) {