diff options
Diffstat (limited to 'src/smt/proof_manager.cpp')
| -rw-r--r-- | src/smt/proof_manager.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index b06590918..f6c489055 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -131,9 +131,10 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n"; - // Now make the final scope, which ensures that the only open leaves - // of the proof are the assertions. - d_finalProof = d_pnm->mkScope(pfn, assertions); + // Now make the final scope, which ensures that the only open leaves of the + // proof are the assertions, unless we are doing proofs to generate unsat + // cores, in which case we do not care. + d_finalProof = d_pnm->mkScope(pfn, assertions, !options::unsatCoresNew()); Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n"; } |