summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/proof_manager.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 9c32abc56..f46317953 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -127,7 +127,7 @@ void ProofManager::traceDeps(TNode n, CDNodeSet* coreAssertions)
}
void ProofManager::traceUnsatCore() {
- Assert(options::unsatCores());
+ Assert(options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF);
d_satProof->refreshProof();
IdToSatClause used_lemmas;
IdToSatClause used_inputs;
@@ -174,7 +174,7 @@ void ProofManager::constructSatProof()
void ProofManager::getLemmasInUnsatCore(std::vector<Node>& lemmas)
{
- Assert(options::unsatCores())
+ Assert(options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
<< "Cannot compute unsat core when proofs are off";
Assert(unsatCoreAvailable())
<< "Cannot get unsat core at this time. Mabye the input is SAT?";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback