mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

#6429

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-23 17:52:14 +07:00
parent 0a671f2f44
commit f87e187b62
2 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -158,6 +158,8 @@ namespace euf {
} }
void egraph::add_literal(enode* n, enode* ante) { void egraph::add_literal(enode* n, enode* ante) {
if (n->bool_var() == sat::null_bool_var)
return;
TRACE("euf_verbose", tout << "lit: " << n->get_expr_id() << "\n";); TRACE("euf_verbose", tout << "lit: " << n->get_expr_id() << "\n";);
m_new_lits.push_back(enode_pair(n, ante)); m_new_lits.push_back(enode_pair(n, ante));
m_updates.push_back(update_record(update_record::new_lit())); m_updates.push_back(update_record(update_record::new_lit()));
@ -272,8 +274,7 @@ namespace euf {
if (enable_merge_tf && n->value() != l_undef && !m.is_value(n->get_root()->get_expr())) { if (enable_merge_tf && n->value() != l_undef && !m.is_value(n->get_root()->get_expr())) {
expr* b = n->value() == l_true ? m.mk_true() : m.mk_false(); expr* b = n->value() == l_true ? m.mk_true() : m.mk_false();
enode* tf = find(b); enode* tf = find(b);
if (!tf) if (tf)
tf = mk(b, 0, 0, nullptr);
add_literal(n, tf); add_literal(n, tf);
} }
} }

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

@ -348,6 +348,8 @@ namespace euf {
continue; continue;
if (!is_relevant(n)) if (!is_relevant(n))
continue; continue;
if (n->bool_var() == sat::null_bool_var)
continue;
bool tt = l_true == s().value(n->bool_var()); bool tt = l_true == s().value(n->bool_var());
if (tt && !mdl.is_false(e)) if (tt && !mdl.is_false(e))
continue; continue;