mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

make euf-egraph resilient to when there are no consumers to literal propagation.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-18 07:57:19 -08:00
parent 3012293c35
commit 9290de8223
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/euf/euf_egraph.cpp
View file

@ -154,10 +154,8 @@ namespace euf {
} }
void egraph::add_literal(enode* n, enode* ante) { void egraph::add_literal(enode* n, enode* ante) {
/* if (!m_on_propagate_literal)
if (n->bool_var() == sat::null_bool_var)
return; return;
*/
if (!ante) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits; if (!ante) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits;
if (!ante) if (!ante)
m_on_propagate_literal(n, ante); m_on_propagate_literal(n, ante);