From 2d7a38e95e2c29ed32b8e75954ea6eac6535e5de Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 13 Dec 2022 16:07:41 -0800
Subject: [PATCH] fix #6488

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifiers/elim_unconstrained.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index bb7a4fa49d8..2e950868a5e 100644
--- 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) {