diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
index cd47da2b1..064688d47 100644
--- 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
index df0606270..86b83af4c 100644
--- 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
index 377db4fc2..b0dc3a9e4 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2077,7 +2077,7 @@ public:
         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];