diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 652663b70..5d0bd4b17 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -298,7 +298,7 @@ namespace euf {
             force_push();
             TRACE("euf", tout << bpp(n) << " := " << value << "\n";);
             n->set_value(value);
-            n->set_justification(j);
+            n->m_lit_justification = j;
             m_updates.push_back(update_record(n, update_record::value_assignment()));
         }
     }
@@ -768,7 +768,7 @@ namespace euf {
                 n->mark1();
                 if (m.is_true(n->get_expr()) || m.is_false(n->get_expr()))
                     continue;
-                justification j = n->m_justification;
+                justification j = n->m_lit_justification;
                 SASSERT(j.is_external());
                 justifications.push_back(j.ext<T>());
             }
diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
index dc98d95c8..7014223be 100644
--- a/src/ast/euf/euf_enode.h
+++ b/src/ast/euf/euf_enode.h
@@ -63,6 +63,7 @@ namespace euf {
         enode*        m_cg     = nullptr;
         th_var_list   m_th_vars;
         justification m_justification;
+        justification m_lit_justification;
         unsigned      m_num_args = 0;
         signed char   m_lbl_hash = -1;  // It is different from -1, if enode is used in a pattern
         approx_set    m_lbls;