#5215

Z3Prover · Apr 28, 2021 · 007b792 · 007b792
1 parent 5ecc32e
commit 007b792
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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;
     }