From 007b792e0f39d45b7a23d866082f6f753cd537cb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Apr 2021 21:05:02 -0700
Subject: [PATCH] #5215

---
 src/sat/smt/euf_internalize.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index d6926566a..2c01118c9 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -157,6 +157,8 @@ namespace euf {
             m_egraph.set_merge_enabled(n, false);
         if (!si.is_bool_op(e))
             track_relevancy(lit.var());
+        if (s().value(lit) != l_undef) 
+            m_egraph.set_value(n, s().value(lit));
         return lit;
     }