mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-21 02:30:23 +00:00
Code Activity

fixing issue where argument equalities for congruence explanations were not updated

Browse source 
explaining equalities added by theories
This commit is contained in:
nilsbecker 2018-05-24 19:25:59 +02:00
parent 9bc7d5de0f
commit 1aeffa2e01
4 changed files with 49 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_context.cpp
View file

@ -562,7 +562,7 @@ namespace smt {
invert_trans(n1);
n1->m_trans.m_target = n2;
n1->m_trans.m_justification = js;
n1->m_proof_is_logged = false;
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
SASSERT(r1->trans_reaches(n1));
// ---------------
// r1 -> .. -> n1 -> n2 -> ... -> r2
@ -748,13 +748,14 @@ namespace smt {
eq_justification js = n->m_trans.m_justification;
prev->m_trans.m_target = nullptr;
prev->m_trans.m_justification = null_eq_justification;
prev->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
while (curr != nullptr) {
SASSERT(prev->trans_reaches(n));
enode * new_curr = curr->m_trans.m_target;
eq_justification new_js = curr->m_trans.m_justification;
curr->m_trans.m_target = prev;
curr->m_trans.m_justification = js;
curr->m_proof_is_logged = false;
curr->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
prev = curr;
js = new_js;
curr = new_curr;
@ -1051,7 +1052,7 @@ namespace smt {
SASSERT(r1->trans_reaches(n1));
n1->m_trans.m_target = nullptr;
n1->m_trans.m_justification = null_eq_justification;
n1->m_proof_is_logged = false;
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
invert_trans(r1);
// ---------------
// n1 -> ... -> r1