From 20d72e5d9771e4d2efca568ccba767d982af6cbc Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 11 Apr 2020 14:37:15 -0400 Subject: [PATCH] (spacer) fix (get-proof) to return proper refutations --- src/muz/spacer/spacer_sat_answer.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_sat_answer.cpp b/src/muz/spacer/spacer_sat_answer.cpp index 9e0a18703..c8b005638 100644 --- a/src/muz/spacer/spacer_sat_answer.cpp +++ b/src/muz/spacer/spacer_sat_answer.cpp @@ -105,7 +105,12 @@ proof_ref ground_sat_answer_op::operator()(pred_transformer &query) { } } 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; }