From 891dcd99c2d7934e4ccf1d69c1d99b23b14a097b Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 21 May 2018 15:22:58 -0700 Subject: [PATCH] Use fact-generating version of mk_unit_resolution() fact-using version of mk_unit_resolution() requires the fact to be a literal. Not sure why this restriction is placed there. --- src/muz/spacer/spacer_proof_utils.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index 151446a93..a2a0ba6b6 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -491,9 +491,10 @@ proof* hypothesis_reducer::mk_unit_resolution_core(proof *ures, } // make unit resolution proof step - expr_ref tmp(m); - tmp = mk_or(m, pf_fact.size(), pf_fact.c_ptr()); - proof* res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), tmp); + // expr_ref tmp(m); + // tmp = mk_or(m, pf_fact.size(), pf_fact.c_ptr()); + // proof* res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), tmp); + proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr()); m_pinned.push_back(res); return res;