mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix equality propagation

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-20 11:09:55 -08:00
parent a475e7cf5a
commit ee04bfd174
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -413,6 +413,8 @@ namespace euf {
m_to_merge.push_back(to_merge(p_other, p, rc.second)); m_to_merge.push_back(to_merge(p_other, p, rc.second));
else else
r2->m_parents.push_back(p); r2->m_parents.push_back(p);
if (p->is_equality())
reinsert_equality(p);
} }
else if (p->is_equality()) { else if (p->is_equality()) {
r2->m_parents.push_back(p); r2->m_parents.push_back(p);
@ -633,7 +635,7 @@ namespace euf {
enode* n = m_todo[i]; enode* n = m_todo[i];
if (n->m_target && !n->is_marked1()) { if (n->m_target && !n->is_marked1()) {
n->mark1(); n->mark1();
CTRACE("euf", m_display_justification, n->m_justification.display(tout << n->get_expr_id() << " = " << n->m_target->get_expr_id() << " ", m_display_justification) << "\n";); CTRACE("euf_verbose", m_display_justification, n->m_justification.display(tout << n->get_expr_id() << " = " << n->m_target->get_expr_id() << " ", m_display_justification) << "\n";);
explain_eq(justifications, n, n->m_target, n->m_justification); explain_eq(justifications, n, n->m_target, n->m_justification);
} }
} }