diff options
Diffstat (limited to 'src/smt/witness_form.cpp')
-rw-r--r-- | src/smt/witness_form.cpp | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 891c0f731..19795119d 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -21,7 +21,12 @@ namespace CVC4 { namespace smt { WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) - : d_tcpg(pnm), d_wintroPf(pnm) + : d_tcpg(pnm, + nullptr, + TConvPolicy::FIXPOINT, + TConvCachePolicy::NEVER, + "WfGenerator::TConvProofGenerator"), + d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof") { } @@ -89,7 +94,13 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) // (exists ((x T)) (P x)) // --------------------------- WITNESS_INTRO // k = (witness ((x T)) (P x)) - d_wintroPf.addLazyStep(exists, pg, false, PfRule::WITNESS_AXIOM); + d_wintroPf.addLazyStep( + exists, + pg, + true, + "WitnessFormGenerator::convertToWitnessForm:witness_axiom", + false, + PfRule::WITNESS_AXIOM); d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {}); d_tcpg.addRewriteStep(cur, curw, &d_wintroPf); } |