Reconciling proofs and unsat cores (#6405)

This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:

the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.

19 files changed, 227 insertions, 172 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 9fb008bfd..4dbd06ce8 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6517,8 +6517,7 @@ std::vector<Term> Solver::getUnsatCore(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]
-                 || d_smtEngine->getOptions()[options::unsatCoresNew])
+  CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
       << "Cannot get unsat core unless explicitly enabled "
          "(try --produce-unsat-cores)";
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 83b83f3be..bb5cc1abe 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -201,27 +201,36 @@ header = "options/smt_options.h"
   help       = "turn on unsat core generation"
 
 [[option]]
-  name       = "checkUnsatCores"
-  category   = "regular"
-  long       = "check-unsat-cores"
-  type       = "bool"
-  help       = "after UNSAT/VALID, produce and check an unsat core (expensive)"
-
-# Temporary option until old unsat cores are removed and this becomes the standard
-[[option]]
-  name       = "unsatCoresNew"
+  name       = "unsatCoresMode"
+  smt_name   = "unsat-cores-mode"
   category   = "regular"
-  long       = "produce-unsat-cores-new"
-  type       = "bool"
-  help       = "turn on unsat core generation using the new proof infrastructure. Note this option is incompatible with the regular unsat cores and with producing proofs."
+  long       = "unsat-cores-mode=MODE"
+  type       = "UnsatCoresMode"
+  default    = "OFF"
+  help       = "choose unsat core mode, see --unsat-cores-mode=help"
+  help_mode  = "unsat cores modes."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not produce unsat cores."
+[[option.mode.OLD_PROOF]]
+  name = "old-proof"
+  help = "Produce unsat cores from old proof infrastructure."
+[[option.mode.SAT_PROOF]]
+  name = "sat-proof"
+  help = "Produce unsat cores from SAT and preprocessing proofs."
+[[option.mode.FULL_PROOF]]
+  name = "full-proof"
+  help = "Produce unsat cores from full proofs."
+[[option.mode.ASSUMPTIONS]]
+  name = "assumptions"
+  help = "Produce unsat cores using solving under assumptions and preprocessing proofs."
 
-# Temporary option until old unsat cores are removed and this becomes the standard
 [[option]]
-  name       = "checkUnsatCoresNew"
+  name       = "checkUnsatCores"
   category   = "regular"
-  long       = "check-unsat-cores-new"
+  long       = "check-unsat-cores"
   type       = "bool"
-  help       = "after UNSAT/VALID, produce and check an unsat core (expensive) using the new proof infrastructure. Note this option is incompatible with the regular unsat cores and with producing proofs."
+  help       = "after UNSAT/VALID, produce and check an unsat core (expensive)"
 
 [[option]]
   name       = "dumpUnsatCores"
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 43f245656..beb8d75af 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -103,7 +103,7 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
   {
     d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
   }
-  else if (options::unsatCores())
+  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::currentPM()->addDependence(n, d_nodes[i]);
   }
@@ -204,7 +204,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
       d_pppg->notifyNewAssert(newConjr, lcp);
     }
   }
-  if (options::unsatCores())
+  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
   }
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index a03ac21a3..2b25098af 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -62,7 +62,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
       imap[assertions->size()] = newSkolems[j];
       assertions->pushBackTrusted(newAsserts[j]);
       // new assertions have a dependence on the node (old pf architecture)
-      if (options::unsatCores())
+      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
       {
         ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
                                                  assertion);
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 8ec75b34d..f2724932f 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -115,7 +115,7 @@ ITESimp::Statistics::Statistics()
 
 bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
 {
-  Assert(!options::unsatCores());
+  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
   bool result = true;
   bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
   if (simpDidALotOfWork)
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 52d6cce3c..893cf0239 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -188,7 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
   Assert(assertionsToPreprocess->getRealAssertionsEnd()
          == assertionsToPreprocess->size());
   Assert(!options::incrementalSolving());
-  Assert(!options::unsatCores());
+  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
 
   context::Context fakeContext;
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 05c53721f..af1e09eca 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -69,8 +69,11 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult NonClausalSimp::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  Assert(!options::unsatCores() || isProofEnabled())
-      << "Unsat cores with non-clausal simp only supported with new proofs";
+  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
+         || isProofEnabled())
+      << "Unsat cores with non-clausal simp only supported with new proofs. "
+         "Cores mode is "
+      << options::unsatCoresMode() << "\n";
 
   d_preprocContext->spendResource(Resource::PreprocessStep);
 
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index cc8820226..90a4b8240 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -59,7 +59,7 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
       imap[assertions->size()] = newSkolems[j];
       assertions->pushBackTrusted(newAsserts[j]);
       // new assertions have a dependence on the node (old pf architecture)
-      if (options::unsatCores())
+      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
       {
         ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
                                                  assertion);
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?";
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 981e51e31..ea30c12e9 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -228,7 +228,7 @@ Solver::Solver(cvc5::prop::TheoryProxy* proxy,
     d_pfManager.reset(
         new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
   }
-  else if (options::unsatCores())
+  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::currentPM()->initSatProof(this);
   }
@@ -241,7 +241,7 @@ Solver::Solver(cvc5::prop::TheoryProxy* proxy,
   uncheckedEnqueue(mkLit(varTrue, false));
   uncheckedEnqueue(mkLit(varFalse, true));
   // FIXME: these should be axioms I believe
-  if (options::unsatCores())
+  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
     ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
@@ -427,7 +427,7 @@ CRef Solver::reason(Var x) {
     // came from (ie. the theory/sharing)
     Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)"
                      << std::endl;
-    if (options::unsatCores())
+    if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
     {
       ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
                                                                 THEORY_LEMMA);
@@ -514,7 +514,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
       lemmas.push();
       ps.copyTo(lemmas.last());
       lemmas_removable.push(removable);
-      if (options::unsatCores())
+      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
       {
         // Store the expression being converted to CNF until
         // the clause is actually created
@@ -533,7 +533,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           // construct the clause below to give to the proof manager
           // as the final conflict.
           if(falseLiteralsCount == 1) {
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               ClauseKind ck =
                   ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -576,7 +576,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
         if (options::unsatCores() || isProofEnabled())
         {
-          if (options::unsatCores())
+          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
           {
             ClauseKind ck =
                 ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -592,7 +592,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           if (ps.size() == falseLiteralsCount)
           {
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               ProofManager::getSatProof()->finalizeProof(cr);
             }
@@ -614,7 +614,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
                          << std::endl;
           if (ps.size() == 1)
           {
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               ClauseKind ck =
                   ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -640,7 +640,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           CRef confl = propagate(CHECK_WITHOUT_THEORY);
           if(! (ok = (confl == CRef_Undef)) ) {
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               if (ca[confl].size() == 1)
               {
@@ -668,7 +668,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           return ok;
         } else {
-          if (options::unsatCores())
+          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
           {
             id = ClauseIdUndef;
           }
@@ -715,7 +715,7 @@ void Solver::detachClause(CRef cr, bool strict) {
       Debug("minisat") << "\n";
     }
     Assert(c.size() > 1);
-    if (options::unsatCores())
+    if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
     {
       ProofManager::getSatProof()->markDeleted(cr);
     }
@@ -997,7 +997,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 
   int max_resolution_level = 0;  // Maximal level of the resolved clauses
 
-  if (options::unsatCores())
+  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::getSatProof()->startResChain(confl);
     }
@@ -1061,7 +1061,8 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
             // FIXME: can we do it lazily if we actually need the proof?
             if (level(var(q)) == 0)
             {
-              if (options::unsatCores())
+              if (options::unsatCoresMode()
+                  == options::UnsatCoresMode::OLD_PROOF)
               {
                 ProofManager::getSatProof()->resolveOutUnit(q);
               }
@@ -1083,7 +1084,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 
         if (pathC > 0 && confl != CRef_Undef)
         {
-          if (options::unsatCores())
+          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
           {
             ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
           }
@@ -1123,7 +1124,8 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                 // Literal is not redundant
                 out_learnt[j++] = out_learnt[i];
               } else {
-                if (options::unsatCores())
+                if (options::unsatCoresMode()
+                    == options::UnsatCoresMode::OLD_PROOF)
                 {
                   ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
                 }
@@ -1419,7 +1421,7 @@ void Solver::propagateTheory() {
         addClause(explanation, true, id);
         // explainPropagation() pushes the explanation on the assertion
         // stack in CnfProof, so we need to pop it here.
-        if (options::unsatCores())
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
         {
           ProofManager::getCnfProof()->popCurrentAssertion();
         }
@@ -1563,7 +1565,8 @@ void Solver::removeSatisfied(vec<CRef>& cs)
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
         if (satisfied(c)) {
-          if (options::unsatCores() && locked(c))
+          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+              && locked(c))
           {
             // store a resolution of the literal c propagated
             ProofManager::getSatProof()->storeUnitResolution(c[0]);
@@ -1670,7 +1673,7 @@ lbool Solver::search(int nof_conflicts)
 
       if (decisionLevel() == 0)
       {
-        if (options::unsatCores())
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
         {
           ProofManager::getSatProof()->finalizeProof(confl);
         }
@@ -1697,7 +1700,7 @@ lbool Solver::search(int nof_conflicts)
       if (learnt_clause.size() == 1)
       {
         uncheckedEnqueue(learnt_clause[0]);
-        if (options::unsatCores())
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
         {
           ProofManager::getSatProof()->endResChain(learnt_clause[0]);
         }
@@ -1715,7 +1718,7 @@ lbool Solver::search(int nof_conflicts)
         attachClause(cr);
         claBumpActivity(ca[cr]);
         uncheckedEnqueue(learnt_clause[0], cr);
-        if (options::unsatCores())
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
         {
           ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
           ProofManager::getSatProof()->endResChain(id);
@@ -2058,8 +2061,10 @@ void Solver::relocAll(ClauseAllocator& to)
             {
               ca.reloc(ws[j].cref,
                        to,
-                       options::unsatCores() ? ProofManager::getSatProof()
-                                             : nullptr);
+                       options::unsatCoresMode()
+                               == options::UnsatCoresMode::OLD_PROOF
+                           ? ProofManager::getSatProof()
+                           : nullptr);
             }
         }
 
@@ -2074,7 +2079,9 @@ void Solver::relocAll(ClauseAllocator& to)
           ca.reloc(
               vardata[v].d_reason,
               to,
-              options::unsatCores() ? ProofManager::getSatProof() : nullptr);
+              options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+                  ? ProofManager::getSatProof()
+                  : nullptr);
         }
     }
     // All learnt:
@@ -2083,7 +2090,9 @@ void Solver::relocAll(ClauseAllocator& to)
     {
       ca.reloc(clauses_removable[i],
                to,
-               options::unsatCores() ? ProofManager::getSatProof() : nullptr);
+               options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+                   ? ProofManager::getSatProof()
+                   : nullptr);
     }
     // All original:
     //
@@ -2091,9 +2100,11 @@ void Solver::relocAll(ClauseAllocator& to)
     {
       ca.reloc(clauses_persistent[i],
                to,
-               options::unsatCores() ? ProofManager::getSatProof() : nullptr);
+               options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+                   ? ProofManager::getSatProof()
+                   : nullptr);
     }
-    if (options::unsatCores())
+    if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
     {
       ProofManager::getSatProof()->finishUpdateCRef();
     }
@@ -2263,7 +2274,7 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      if (options::unsatCores())
+      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
       {
         TNode cnf_assertion = lemmas_cnf_assertion[j];
 
@@ -2284,7 +2295,8 @@ CRef Solver::updateLemmas() {
     // If the lemma is propagating enqueue its literal (or set the conflict)
     if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
       if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
-        if (options::unsatCores() && lemma.size() == 1)
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+            && lemma.size() == 1)
         {
           Node cnf_assertion = lemmas_cnf_assertion[j];
 
@@ -2304,7 +2316,7 @@ CRef Solver::updateLemmas() {
           } else {
             Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
             conflict = CRef_Lazy;
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
             }
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());
 }
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 51ce2ced2..98a76ae1a 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -98,10 +98,11 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   Node theoryExplanation = tte.getNode();
   if (options::produceProofs())
   {
-    Assert(options::unsatCoresNew() || tte.getGenerator());
+    Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
+           || tte.getGenerator());
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }
-  else if (options::unsatCores())
+  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
   }
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index aee7a2a86..2fb83f898 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -178,7 +178,7 @@ void Assertions::addFormula(
   }
 
   // Give it to the old proof manager
-  if (options::unsatCores())
+  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     if (inInput)
     {  // n is an input assertion
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index f6c489055..422efac6a 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -134,7 +134,7 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
   // 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());
+  d_finalProof = d_pnm->mkScope(pfn, assertions, !options::unsatCores());
   Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
 }
 
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index e34947be6..60e93306a 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -46,13 +46,24 @@ class ProofPostproccess;
  *   SmtEngine will not have proofs in the sense of this proof manager.
  *
  * - If we are producing unsat cores using this proof infrastructure, then the
- *   SmtEngine will have proofs using this proof manager (if --produce-proofs
- *   was not passed by the user it will be activated), but these proofs will
- *   only cover preprocessing and the prop engine, i.e., the theory engine will
- *   not have proofs.
+ *   SmtEngine will have proofs using this proof manager, according to the unsat
+ *   core mode:
+ *
+ *   - assumption mode: proofs only for preprocessing, not in sat solver or
+ *   theory engine, and level of granularity set to off (unless otherwise
+ *   specified by the user)
+ *
+ *   - sat-proof mode: proofs for preprocessing + sat solver, not in theory
+ *   engine and level of granularity set to off (unless otherwise specified by
+ *   the user)
+ *
+ *   - full-proof mode: proofs for the whole solver as normal
+ *
+ *   Note that if --produce-proofs is set then full-proof mode of unsat cores is
+ *   forced.
  *
  * - If we are not producing unsat cores then the SmtEngine will have proofs as
- *   long as --produce-proofs was given.
+ *   long as --produce-proofs is on.
  *
  * - If SmtEngine has been configured in a way that is incompatible with proofs
  *   then unsat core production will be disabled.
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index cf5fc267b..aaeb8e0aa 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -52,59 +52,82 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // implied options
   if (options::debugCheckModels())
   {
-    Notice() << "SmtEngine: setting checkModel" << std::endl;
     options::checkModels.set(true);
   }
   if (options::checkModels() || options::dumpModels())
   {
-    Notice() << "SmtEngine: setting produceModels" << std::endl;
     options::produceModels.set(true);
   }
   if (options::checkModels())
   {
-    Notice() << "SmtEngine: setting produceAssignments" << std::endl;
     options::produceAssignments.set(true);
   }
+  // unsat cores and proofs shenanigans
   if (options::dumpUnsatCoresFull())
   {
-    Notice() << "SmtEngine: setting dumpUnsatCores" << std::endl;
     options::dumpUnsatCores.set(true);
   }
-  if ((options::unsatCores() && options::unsatCoresNew())
-      || (options::checkUnsatCores() && options::checkUnsatCoresNew()))
+  if (options::checkUnsatCores() || options::dumpUnsatCores()
+      || options::unsatAssumptions())
   {
-    AlwaysAssert(false) << "Can't have both unsat cores modes, pick one.\n";
+    options::unsatCores.set(true);
   }
-  if (options::checkUnsatCores())
+
+  if (options::unsatCores()
+      && options::unsatCoresMode() == options::UnsatCoresMode::OFF)
   {
-    options::unsatCores.set(true);
+    if (options::unsatCoresMode.wasSetByUser())
+    {
+      Notice()
+          << "Overriding OFF unsat-core mode since cores were requested..\n";
+    }
+    options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
   }
-  if (options::checkUnsatCoresNew())
+
+  if (options::checkProofs() || options::dumpProofs())
   {
-    options::unsatCoresNew.set(true);
+    options::produceProofs.set(true);
   }
-  if (options::dumpUnsatCores() || options::unsatAssumptions())
+
+  if (options::produceProofs()
+      && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
   {
-    if (!options::unsatCoresNew())
+    if (options::unsatCoresMode.wasSetByUser())
     {
-      Notice() << "SmtEngine: setting unsatCores" << std::endl;
-      options::unsatCores.set(true);
+      Notice() << "Forcing full-proof mode for unsat cores mode since proofs "
+                  "were requested.\n";
     }
+    options::unsatCoresMode.set(options::UnsatCoresMode::FULL_PROOF);
   }
-  if (options::unsatCoresNew()
-      && ((options::produceProofs() && options::produceProofs.wasSetByUser())
-          || (options::checkProofs() && options::checkProofs.wasSetByUser())
-          || (options::dumpProofs() && options::dumpProofs.wasSetByUser())))
+
+  // set proofs on if not yet set
+  if (options::unsatCores() && !options::produceProofs()
+      && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF)
   {
-    AlwaysAssert(false) << "Can't properly produce proofs and have the new "
-                           "unsat cores simultaneously.\n";
+    if (options::produceProofs.wasSetByUser())
+    {
+      Notice()
+          << "Forcing proof production since new unsat cores were requested.\n";
+    }
+    options::produceProofs.set(true);
   }
-  if (options::checkProofs() || options::unsatCoresNew()
-      || options::dumpProofs())
+
+  // guarantee that if unsat cores mode is not OFF, then they are activated
+  if (!options::unsatCores())
   {
-    Notice() << "SmtEngine: setting proof" << std::endl;
-    options::produceProofs.set(true);
+    if (options::unsatCoresMode.wasSetByUser())
+    {
+      Notice() << "Overriding unsat-core mode for OFF since cores were not "
+                  "requested.\n";
+    }
+    options::unsatCoresMode.set(options::UnsatCoresMode::OFF);
   }
+
+  // whether we want to force safe unsat cores, i.e., if we are in the OLD_PROOF
+  // unsat core mode, since new ones are experimental
+  bool safeUnsatCores =
+      options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF;
+
   if (options::bitvectorAigSimplifications.wasSetByUser())
   {
     Notice() << "SmtEngine: setting bitvectorAig" << std::endl;
@@ -299,15 +322,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // formulas is unsat. Thus, proofs do not apply.
     disableProofs = true;
   }
-  // !!! must disable proofs if using the old unsat core infrastructure
-  // TODO (#project 37) remove this
-  if (options::unsatCores())
-  {
-    disableProofs = true;
-  }
 
   // new unsat core specific restrictions for proofs
-  if (options::unsatCoresNew())
+  if (options::unsatCores()
+      && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
+      && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
   {
     // no fine-graininess
     if (!options::proofGranularityMode.wasSetByUser())
@@ -368,12 +387,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // if we requiring disabling proofs, disable them now
   if (disableProofs && options::produceProofs())
   {
-    if (options::unsatCoresNew())
+    if (options::unsatCoresMode() != options::UnsatCoresMode::OFF
+        && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF)
     {
-      Notice() << "SmtEngine: turning off new unsat cores." << std::endl;
+      Notice() << "SmtEngine: reverting to old unsat cores since proofs are "
+                  "disabled.\n";
+      options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
     }
-    options::unsatCoresNew.set(false);
-    options::checkUnsatCoresNew.set(false);
     if (options::produceProofs())
     {
       Notice() << "SmtEngine: turning off produce-proofs." << std::endl;
@@ -387,6 +407,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::sygusCoreConnective())
   {
     options::unsatCores.set(true);
+    if (options::unsatCoresMode() == options::UnsatCoresMode::OFF)
+    {
+      options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
+    }
   }
 
   if ((options::checkModels() || options::checkSynthSol()
@@ -405,19 +429,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // Disable options incompatible with incremental solving, unsat cores or
   // output an error if enabled explicitly. It is also currently incompatible
   // with arithmetic, force the option off.
-  if (options::incrementalSolving() || options::unsatCores()
-      || options::unsatCoresNew())
+  if (options::incrementalSolving() || safeUnsatCores)
   {
     if (options::unconstrainedSimp())
     {
       if (options::unconstrainedSimp.wasSetByUser())
       {
         throw OptionException(
-            "unconstrained simplification not supported with unsat "
+            "unconstrained simplification not supported with old unsat "
             "cores/incremental solving");
       }
       Notice() << "SmtEngine: turning off unconstrained simplification to "
-                  "support unsat cores/incremental solving"
+                  "support old unsat cores/incremental solving"
                << std::endl;
       options::unconstrainedSimp.set(false);
     }
@@ -468,13 +491,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   // Disable options incompatible with unsat cores or output an error if enabled
   // explicitly
-  if (options::unsatCores() || options::unsatCoresNew())
+  if (safeUnsatCores)
   {
     if (options::simplificationMode() != options::SimplificationMode::NONE)
     {
       if (options::simplificationMode.wasSetByUser())
       {
-        throw OptionException("simplification not supported with unsat cores");
+        throw OptionException(
+            "simplification not supported with old unsat cores");
       }
       Notice() << "SmtEngine: turning off simplification to support unsat "
                   "cores"
@@ -487,11 +511,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       if (options::pbRewrites.wasSetByUser())
       {
         throw OptionException(
-            "pseudoboolean rewrites not supported with unsat cores");
+            "pseudoboolean rewrites not supported with old unsat cores");
       }
       Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
-                  "unsat cores"
-               << std::endl;
+                  "old unsat cores\n";
       options::pbRewrites.set(false);
     }
 
@@ -499,11 +522,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       if (options::sortInference.wasSetByUser())
       {
-        throw OptionException("sort inference not supported with unsat cores");
+        throw OptionException(
+            "sort inference not supported with old unsat cores");
       }
-      Notice() << "SmtEngine: turning off sort inference to support unsat "
-                  "cores"
-               << std::endl;
+      Notice() << "SmtEngine: turning off sort inference to support old unsat "
+                  "cores\n";
       options::sortInference.set(false);
     }
 
@@ -512,24 +535,21 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       if (options::preSkolemQuant.wasSetByUser())
       {
         throw OptionException(
-            "pre-skolemization not supported with unsat cores");
+            "pre-skolemization not supported with old unsat cores");
       }
-      Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
-                  "cores"
-               << std::endl;
+      Notice() << "SmtEngine: turning off pre-skolemization to support old "
+                  "unsat cores\n";
       options::preSkolemQuant.set(false);
     }
 
-
     if (options::bitvectorToBool())
     {
       if (options::bitvectorToBool.wasSetByUser())
       {
-        throw OptionException("bv-to-bool not supported with unsat cores");
+        throw OptionException("bv-to-bool not supported with old unsat cores");
       }
-      Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
-                  "cores"
-               << std::endl;
+      Notice() << "SmtEngine: turning off bitvector-to-bool to support old "
+                  "unsat cores\n";
       options::bitvectorToBool.set(false);
     }
 
@@ -538,11 +558,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       if (options::boolToBitvector.wasSetByUser())
       {
         throw OptionException(
-            "bool-to-bv != off not supported with unsat cores");
+            "bool-to-bv != off not supported with old unsat cores");
       }
-      Notice() << "SmtEngine: turning off bool-to-bv to support unsat "
-                  "cores"
-               << std::endl;
+      Notice()
+          << "SmtEngine: turning off bool-to-bv to support old unsat cores\n";
       options::boolToBitvector.set(options::BoolToBVMode::OFF);
     }
 
@@ -550,11 +569,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       if (options::bvIntroducePow2.wasSetByUser())
       {
-        throw OptionException("bv-intro-pow2 not supported with unsat cores");
+        throw OptionException(
+            "bv-intro-pow2 not supported with old unsat cores");
       }
-      Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
-                  "unsat-cores"
-               << std::endl;
+      Notice()
+          << "SmtEngine: turning off bv-intro-pow2 to support old unsat cores";
       options::bvIntroducePow2.set(false);
     }
 
@@ -562,11 +581,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       if (options::repeatSimp.wasSetByUser())
       {
-        throw OptionException("repeat-simp not supported with unsat cores");
+        throw OptionException("repeat-simp not supported with old unsat cores");
       }
-      Notice() << "SmtEngine: turning off repeat-simp to support unsat "
-                  "cores"
-               << std::endl;
+      Notice()
+          << "SmtEngine: turning off repeat-simp to support old unsat cores\n";
       options::repeatSimp.set(false);
     }
 
@@ -574,22 +592,22 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       if (options::globalNegate.wasSetByUser())
       {
-        throw OptionException("global-negate not supported with unsat cores");
+        throw OptionException(
+            "global-negate not supported with old unsat cores");
       }
-      Notice() << "SmtEngine: turning off global-negate to support unsat "
-                  "cores"
-               << std::endl;
+      Notice() << "SmtEngine: turning off global-negate to support old unsat "
+                  "cores\n";
       options::globalNegate.set(false);
     }
 
     if (options::bitvectorAig())
     {
-      throw OptionException("bitblast-aig not supported with unsat cores");
+      throw OptionException("bitblast-aig not supported with old unsat cores");
     }
 
     if (options::doITESimp())
     {
-      throw OptionException("ITE simp not supported with unsat cores");
+      throw OptionException("ITE simp not supported with old unsat cores");
     }
   }
   else
@@ -746,8 +764,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (!options::ufSymmetryBreaker.wasSetByUser())
   {
     bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
-                       && !options::incrementalSolving()
-                       && !options::unsatCores() && !options::unsatCoresNew();
+                       && !options::incrementalSolving() && !safeUnsatCores;
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
                  << std::endl;
     options::ufSymmetryBreaker.set(qf_uf_noinc);
@@ -796,7 +813,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                       && (logic.isTheoryEnabled(THEORY_ARRAYS)
                           && logic.isTheoryEnabled(THEORY_UF)
                           && logic.isTheoryEnabled(THEORY_BV))
-                      && !options::unsatCores() && !options::unsatCoresNew();
+                      && !safeUnsatCores;
     Trace("smt") << "setting repeat simplification to " << repeatSimp
                  << std::endl;
     options::repeatSimp.set(repeatSimp);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3e64c5d23..8e8a1e062 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -235,10 +235,7 @@ void SmtEngine::finishInit()
   }
 
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
-  // if proofs and unsat cores, proofs are used solely for unsat core
-  // production, so we don't generate proofs in the theory engine, which is
-  // communicated via the second argument
-  d_smtSolver->finishInit(logic, options::unsatCoresNew());
+  d_smtSolver->finishInit(logic);
 
   // now can construct the SMT-level model object
   TheoryEngine* te = d_smtSolver->getTheoryEngine();
@@ -962,7 +959,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate an unsat core correctly.
-    if (options::checkUnsatCores() || options::checkUnsatCoresNew())
+    if (options::checkUnsatCores())
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
@@ -1401,11 +1398,11 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry()
 
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
-  if (!options::unsatCores() && !options::unsatCoresNew())
+  if (!options::unsatCores())
   {
     throw ModalException(
-        "Cannot get an unsat core when produce-unsat-cores[-new] option is "
-        "off.");
+        "Cannot get an unsat core when produce-unsat-cores[-new] or "
+        "produce-proofs option is off.");
   }
   if (d_state->getMode() != SmtMode::UNSAT)
   {
@@ -1431,7 +1428,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
 }
 
 void SmtEngine::checkUnsatCore() {
-  Assert(options::unsatCores() || options::unsatCoresNew())
+  Assert(options::unsatCores())
       << "cannot check unsat core if unsat cores are turned off";
 
   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
@@ -1444,7 +1441,6 @@ void SmtEngine::checkUnsatCore() {
   // disable all proof options
   coreChecker->getOptions().set(options::produceProofs, false);
   coreChecker->getOptions().set(options::checkProofs, false);
-  coreChecker->getOptions().set(options::checkUnsatCoresNew, false);
   coreChecker->getOptions().set(options::proofEagerChecking, false);
 
   // set up separation logic heap if necessary
@@ -1630,7 +1626,9 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (options::produceProofs() && !options::unsatCoresNew()
+  if (options::produceProofs()
+      && (!options::unsatCores()
+          || options::unsatCoresMode() == options::UnsatCoresMode::FULL_PROOF)
       && getSmtMode() == SmtMode::UNSAT)
   {
     // minimize instantiations based on proof manager
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 2847e5ee9..4c841ce9c 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -49,18 +49,23 @@ SmtSolver::SmtSolver(SmtEngine& smt,
 
 SmtSolver::~SmtSolver() {}
 
-void SmtSolver::finishInit(const LogicInfo& logicInfo,
-                           bool proofForUnsatCoreMode)
+void SmtSolver::finishInit(const LogicInfo& logicInfo)
 {
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine.reset(
-      new TheoryEngine(d_smt.getContext(),
-                       d_smt.getUserContext(),
-                       d_rm,
-                       logicInfo,
-                       d_smt.getOutputManager(),
-                       proofForUnsatCoreMode ? nullptr : d_pnm));
+  d_theoryEngine.reset(new TheoryEngine(
+      d_smt.getContext(),
+      d_smt.getUserContext(),
+      d_rm,
+      logicInfo,
+      d_smt.getOutputManager(),
+      // Other than whether d_pm is set, theory engine proofs are conditioned on
+      // the relationshup between proofs and unsat cores: the unsat cores are in
+      // FULL_PROOF mode, no proofs are generated on theory engine.
+      (options::unsatCores()
+       && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
+          ? nullptr
+          : d_pnm));
 
   // Add the theories
   for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index b02cde88a..8689f152c 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -73,11 +73,8 @@ class SmtSolver
    * Create theory engine, prop engine based on the logic info.
    *
    * @param logicInfo the logic information
-   * @param proofForUnsatCoreMode whether this SmtSolver will operate in unsat
-   * core mode. If true, proofs will not be produced in the theory engine.
    */
-  void finishInit(const LogicInfo& logicInfo,
-                  bool proofForUnsatCoreMode = false);
+  void finishInit(const LogicInfo& logicInfo);
   /** Reset all assertions, global declarations, etc.  */
   void resetAssertions();
   /**