diff options
Diffstat (limited to 'src/expr/proof_generator.cpp')
| -rw-r--r-- | src/expr/proof_generator.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index 2d114acd6..93f291e9a 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -43,7 +43,10 @@ std::shared_ptr<ProofNode> ProofGenerator::getProofFor(Node f) return nullptr; } -bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy) +bool ProofGenerator::addProofTo(Node f, + CDProof* pf, + CDPOverwrite opolicy, + bool doCopy) { Trace("pfgen") << "ProofGenerator::addProofTo: " << f << "..." << std::endl; Assert(pf != nullptr); @@ -52,8 +55,7 @@ bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy) if (apf != nullptr) { Trace("pfgen") << "...got proof " << *apf.get() << std::endl; - // Add the proof, without deep copying. - if (pf->addProof(apf, opolicy, false)) + if (pf->addProof(apf, opolicy, doCopy)) { Trace("pfgen") << "...success!" << std::endl; return true; |