mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

fix #6488

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-13 16:07:41 -08:00
parent 7afcaa5364
commit 2d7a38e95e
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -65,7 +65,6 @@ void elim_unconstrained::eliminate() {
expr_ref r(m), side_cond(m); expr_ref r(m), side_cond(m);
int v = m_heap.erase_min(); int v = m_heap.erase_min();
node& n = get_node(v); 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) if (n.m_refcount == 0)
continue; continue;
if (n.m_refcount > 1) if (n.m_refcount > 1)
@ -203,10 +202,11 @@ void elim_unconstrained::freeze(expr* t) {
return; return;
node& n = get_node(t); node& n = get_node(t);
if (!n.m_term) if (!n.m_term)
return; return;
n.m_refcount = UINT_MAX / 2; if (m_heap.contains(root(t))) {
if (m_heap.contains(root(t))) n.m_refcount = UINT_MAX / 2;
m_heap.increased(root(t)); m_heap.increased(root(t));
}
} }
void elim_unconstrained::gc(expr* t) { void elim_unconstrained::gc(expr* t) {