mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5215

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-27 21:05:02 -07:00
parent 5ecc32e731
commit 007b792e0f
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/euf_internalize.cpp
View file

@ -157,6 +157,8 @@ namespace euf {
m_egraph.set_merge_enabled(n, false); m_egraph.set_merge_enabled(n, false);
if (!si.is_bool_op(e)) if (!si.is_bool_op(e))
track_relevancy(lit.var()); track_relevancy(lit.var());
if (s().value(lit) != l_undef)
m_egraph.set_value(n, s().value(lit));
return lit; return lit;
} }