fix Z3Prover#6488

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
hgvk94 · Mar 27, 2023 · 1367ecd · 1367ecd
1 parent 2a12b8d
commit 1367ecd
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -65,7 +65,6 @@ void elim_unconstrained::eliminate() {
         expr_ref r(m), side_cond(m);
         int v = m_heap.erase_min();
         node& n = get_node(v);
-        IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(n.m_orig, m) << " @ " << n.m_refcount << "\n");
         if (n.m_refcount == 0)
             continue;
         if (n.m_refcount > 1)
@@ -203,10 +202,11 @@ void elim_unconstrained::freeze(expr* t) {
         return;
     node& n = get_node(t);
     if (!n.m_term)
-        return;
-    n.m_refcount = UINT_MAX / 2;
-    if (m_heap.contains(root(t)))
+        return;    
+    if (m_heap.contains(root(t))) {
+        n.m_refcount = UINT_MAX / 2;
         m_heap.increased(root(t));
+    }
 }
 
 void elim_unconstrained::gc(expr* t) {