mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

#5417

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-19 13:41:02 -07:00
parent b0a22105d6
commit 0a34eef470
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/euf_solver.cpp
View file

@ -348,9 +348,7 @@ namespace euf {
void solver::propagate_literals() { void solver::propagate_literals() {
for (; m_egraph.has_literal() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_literal()) { for (; m_egraph.has_literal() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_literal()) {
euf::enode_bool_pair p = m_egraph.get_literal(); auto [n, is_eq] = m_egraph.get_literal();
euf::enode* n = p.first;
bool is_eq = p.second;
expr* e = n->get_expr(); expr* e = n->get_expr();
expr* a = nullptr, *b = nullptr; expr* a = nullptr, *b = nullptr;
bool_var v = n->bool_var(); bool_var v = n->bool_var();
@ -364,6 +362,10 @@ namespace euf {
} }
else { else {
lbool val = n->get_root()->value(); lbool val = n->get_root()->value();
if (val == l_undef && m.is_false(n->get_root()->get_expr()))
val = l_false;
if (val == l_undef && m.is_true(n->get_root()->get_expr()))
val = l_true;
a = e; a = e;
b = (val == l_true) ? m.mk_true() : m.mk_false(); b = (val == l_true) ? m.mk_true() : m.mk_false();
SASSERT(val != l_undef); SASSERT(val != l_undef);