From 9290de822394af0a1efb2bb23b1ff8ee17783b1b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Jan 2023 07:57:19 -0800 Subject: [PATCH] make euf-egraph resilient to when there are no consumers to literal propagation. Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) 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);