mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

(spacer) fix (get-proof) to return proper refutations

Browse source
This commit is contained in:
Arie Gurfinkel 2020-04-11 14:37:15 -04:00
parent 76c2fb5732
commit 20d72e5d97
1 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz/spacer/spacer_sat_answer.cpp
View file

@ -105,7 +105,12 @@ proof_ref ground_sat_answer_op::operator()(pred_transformer &query) {
} }
} }
m_solver.reset(); m_solver.reset();
return proof_ref(m_cache.find(root_fact), m);
// turn proof of root fact into a refutation
proof_ref pf1(m_cache.find(root_fact), m);
proof_ref pf2(m.mk_asserted(m.mk_implies(m.get_fact(pf1), m.mk_false())), m);
pf1 = m.mk_modus_ponens(pf1, pf2);
return pf1;
} }