fix #6978

Z3Prover · Nov 14, 2023 · ad2107f · ad2107f
1 parent 4406011
commit ad2107f
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 2 deletions.
diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
@@ -97,6 +97,7 @@ namespace euf {
             for (unsigned i = 0; i < num_args; ++i) {
                 SASSERT(to_app(f)->get_arg(i) == args[i]->get_expr());
                 n->m_args[i] = args[i];
+                n->m_args[i]->get_root()->set_is_shared(l_undef);
             }
             return n;
         }

diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
@@ -54,7 +54,7 @@ namespace smt {
         for (unsigned i = 0; i < num_args; i++) {            
             enode * arg  = app2enode[owner->get_arg(i)->get_id()];
             n->m_args[i] = arg;
-            arg->m_is_shared = 2;
+            arg->get_root()->m_is_shared = 2;
             SASSERT(n->get_arg(i) == arg);
             if (update_children_parent)
                 arg->get_root()->m_parents.push_back(n);

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -2077,7 +2077,7 @@ class theory_lra::imp {
         enode * n      = get_enode(v);
         enode * r      = n->get_root();
         unsigned usz   = m_underspecified.size();
-        TRACE("shared", tout << ctx().get_scope_level() << " " <<  v << " " << r->get_num_parents() << "\n";);
+        TRACE("shared", tout << ctx().get_scope_level() << " " <<  enode_pp(n, ctx()) << " " << v << " underspecified " << usz << " parents " << r->get_num_parents() << "\n";);
         if (r->get_num_parents() > 2*usz) {
             for (unsigned i = 0; i < usz; ++i) {
                 app* u = m_underspecified[i];