diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
| -rw-r--r-- | src/prop/prop_engine.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2eaa3a812..646da84b2 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -122,7 +122,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_ppm.reset( new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get())); } - else if (options::unsatCores()) + else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) { ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext); } @@ -246,8 +246,11 @@ void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn, Node node = trn.getNode(); Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl; bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; - Assert(!isProofEnabled() || trn.getGenerator() != nullptr - || options::unsatCores() || options::unsatCoresNew()); + Assert( + !isProofEnabled() || trn.getGenerator() != nullptr + || options::unsatCores() + || (options::unsatCores() + && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)); assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator()); } |