diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 115a3f53f..7939c23f2 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -154,10 +154,8 @@ namespace euf { } void egraph::add_literal(enode* n, enode* ante) { - /* - if (n->bool_var() == sat::null_bool_var) + if (!m_on_propagate_literal) return; - */ if (!ante) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits; if (!ante) m_on_propagate_literal(n, ante);