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; }