diff options
Diffstat (limited to 'src/smt/proof_manager.cpp')
| -rw-r--r-- | src/smt/proof_manager.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 5b938ab64..b651e390c 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -19,6 +19,7 @@ #include "expr/proof_node_manager.h" #include "options/base_options.h" #include "options/proof_options.h" +#include "options/smt_options.h" #include "proof/dot/dot_printer.h" #include "smt/assertions.h" #include "smt/defined_function.h" @@ -121,6 +122,13 @@ void PfManager::printProof(std::ostream& out, { Trace("smt-proof") << "PfManager::printProof: start" << std::endl; std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df); + // if we are in incremental mode, we don't want to invalidate the proof + // nodes in fp, since these may be reused in further check-sat calls + if (options::incrementalSolving() + && options::proofFormatMode() != options::ProofFormatMode::NONE) + { + fp = d_pnm->clone(fp); + } // TODO (proj #37) according to the proof format, post process the proof node // TODO (proj #37) according to the proof format, print the proof node |