From 815c971c9ac85669b5f16b82821ef5a1d2d2d801 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 22 Mar 2022 01:55:43 -0700
Subject: [PATCH] #5778

regression when tracking literal explanations
---
 src/ast/euf/euf_egraph.cpp | 4 ++--
 src/ast/euf/euf_enode.h    | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

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;