diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-02 10:28:36 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-02 15:28:36 +0000 |
| commit | ec6fe33ab778a7bb5d2d016b799b1918b90fc338 (patch) | |
| tree | a870fea033a8cbf0761d7574c773b18e05f32a2e /src/smt/proof_manager.cpp | |
| parent | c54fe84863ce4257bd466a95ec42d7a6100d3c19 (diff) | |
Fix unsat core proofs (#6655)
Fixes cases of satisfiable unsat cores when proofs are enabled.
Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.
Diffstat (limited to 'src/smt/proof_manager.cpp')
| -rw-r--r-- | src/smt/proof_manager.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index ad1e40c77..55cfc1f15 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -130,9 +130,8 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as) 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, unless we are doing proofs to generate unsat - // cores, in which case we do not care. - d_finalProof = d_pnm->mkScope(pfn, assertions, !options::unsatCores()); + // proof are the assertions. + d_finalProof = d_pnm->mkScope(pfn, assertions); Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n"; } |