mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix #4932

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-08 12:50:36 -08:00
parent 3d39f37e63
commit 43eb862374
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_conflict_resolution.cpp
View file

@ -794,6 +794,11 @@ namespace smt {
if (is_eq && is_quantifier(f2)) {
f2 = m_ctx.get_enode(f2)->get_owner();
}
if (m.is_false(fact) && !m_ctx.is_true(n2) && !m_ctx.is_false(n2)) {
pr = m.mk_hypothesis(m.mk_eq(n1_owner, n2_owner));
m_new_proofs.push_back(pr);
return pr;
}
if (!is_eq || (f1 != n2_owner && f2 != n2_owner)) {
CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2),
tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n";