fix #6488

Z3Prover · Dec 12, 2022 · a3e6885 · a3e6885 · nunoplopes · Dec 12, 2022
1 parent 039de6a
commit a3e6885
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 9 deletions.
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -96,7 +96,7 @@ void elim_unconstrained::eliminate() {
         m_trail.push_back(r);
         SASSERT(r);
         gc(e);
-        init_children(e, r);
+        freeze_rec(r);
 
         m_root.setx(r->get_id(), e->get_id(), UINT_MAX);
         get_node(e).m_term = r;
@@ -180,9 +180,8 @@ void elim_unconstrained::init_terms(expr_ref_vector const& terms) {
     }
 }
 
-void elim_unconstrained::init_children(expr* e, expr* r) {
+void elim_unconstrained::freeze_rec(expr* r) {
     expr_ref_vector children(m);
-    SASSERT(e != r);
     if (is_quantifier(r))
         children.push_back(to_quantifier(r)->get_expr());
     else if (is_app(r))
@@ -191,11 +190,20 @@ void elim_unconstrained::init_children(expr* e, expr* r) {
         return;
     if (children.empty())
         return;
-    init_terms(children);
-    for (expr* arg : children) {
-        get_node(arg).m_parents.push_back(e);
-        inc_ref(arg);
-    }
+    for (expr* t : subterms::all(children))
+        freeze(t);
+}
+
+void elim_unconstrained::freeze(expr* t) {
+    if (!is_uninterp_const(t))
+        return;
+    if (m_nodes.size() <= t->get_id())
+        return;
+    node& n = get_node(t);
+    if (!n.m_term)
+        return;
+    n.m_refcount = UINT_MAX / 2;
+    m_heap.increased(root(t));
 }
 
 void elim_unconstrained::gc(expr* t) {

diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h
@@ -58,8 +58,9 @@ class elim_unconstrained : public dependent_expr_simplifier {
     unsigned get_refcount(expr* t) const { return get_node(t).m_refcount; }
     void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(root(t)); }
     void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(root(t)); }
+    void freeze(expr* t);
+    void freeze_rec(expr* r);
     void gc(expr* t);
-    void init_children(expr* e, expr* r);
     expr* get_parent(unsigned n) const;
     void init_terms(expr_ref_vector const& terms);
     void init_nodes();