diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp index e1489bef2..b8351fe14 100644 --- a/src/sat/smt/polysat_egraph.cpp +++ b/src/sat/smt/polysat_egraph.cpp @@ -204,8 +204,7 @@ namespace polysat { if (slice.child != null_var) { auto c = var2enode(m_pddvar2var[slice.child]); - if (b != c) - m_bv_plugin->explain_slice(b, 0, c, consume_eq); + m_bv_plugin->explain_slice(b, 0, c, consume_eq); } }