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

Use fact-generating version of mk_unit_resolution()

Browse source 
fact-using version of mk_unit_resolution() requires the fact to be a
literal. Not sure why this restriction is placed there.
This commit is contained in:
Arie Gurfinkel 2018-05-21 15:22:58 -07:00
parent 8be03f7c1f
commit 891dcd99c2
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -491,9 +491,10 @@ proof* hypothesis_reducer::mk_unit_resolution_core(proof *ures,
} }
// make unit resolution proof step // make unit resolution proof step
expr_ref tmp(m); // expr_ref tmp(m);
tmp = mk_or(m, pf_fact.size(), pf_fact.c_ptr()); // 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(), tmp);
proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr());
m_pinned.push_back(res); m_pinned.push_back(res);
return res; return res;