mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
parent
b954e0d64b
commit
cb136418d5
|
@ -463,6 +463,8 @@ public:
|
|||
reduce_hypotheses0(ast_manager& m): m(m), m_refs(m) {}
|
||||
|
||||
void operator()(proof_ref& pr) {
|
||||
if (!pr)
|
||||
throw default_exception("proof reduction requires well defined proofs");
|
||||
proof_ref tmp(m);
|
||||
tmp = pr;
|
||||
elim(pr);
|
||||
|
|
Loading…
Reference in a new issue