From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 14 Apr 2021 17:50:10 +0000 (-0300)
Subject: [unsat-cores] Improving new unsat cores (#6356)
X-Git-Tag: cvc5-1.0.0~1905
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b6db4446a28d498af8fb4e629392985dfe2a976c;p=cvc5.git

[unsat-cores] Improving new unsat cores (#6356)

This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.

This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 435597bc7..1c62bd4f0 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6256,7 +6256,8 @@ std::vector<Term> Solver::getUnsatCore(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
+  CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]
+                 || d_smtEngine->getOptions()[options::unsatCoresNew])
       << "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 c8a1a8fb4..c6e42477b 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -207,12 +207,21 @@ header = "options/smt_options.h"
   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"
+  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."
+
+# Temporary option until old unsat cores are removed and this becomes the standard
 [[option]]
   name       = "checkUnsatCoresNew"
   category   = "regular"
   long       = "check-unsat-cores-new"
   type       = "bool"
-  help       = "after UNSAT/VALID, produce and check an unsat core (expensive) using the new proof infrastructure"
+  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."
 
 [[option]]
   name       = "dumpUnsatCores"
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 7d21066d8..43f245656 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -204,7 +204,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
       d_pppg->notifyNewAssert(newConjr, lcp);
     }
   }
-  if (options::unsatCores() && !isProofEnabled())
+  if (options::unsatCores())
   {
     ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
   }
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 068e47f13..a03ac21a3 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() && !options::produceProofs())
+      if (options::unsatCores())
       {
         ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
                                                  assertion);
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 66837267a..952ced4d5 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -86,7 +86,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap)
     for( int i=0; i<(int)assertions.size(); i++ ){
       Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
       if( processAssertion( assertions[i] ) ){
-        if (options::unsatCores() && !options::produceProofs()
+        if (options::unsatCores()
             && std::find(macro_assertions.begin(),
                          macro_assertions.end(),
                          assertions[i])
@@ -116,7 +116,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap)
           // is an over-approximation. a more fine-grained unsat core
           // computation would require caching dependencies for each subterm of
           // the formula, which is expensive.
-          if (options::unsatCores() && !options::produceProofs())
+          if (options::unsatCores())
           {
             ProofManager::currentPM()->addDependence(curr, assertions[i]);
             for (unsigned j = 0; j < macro_assertions.size(); j++)
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 7a7809eef..8f59ec13b 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -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() && !isProofEnabled())
+  if (options::unsatCores())
   {
     ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
     ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
@@ -344,7 +344,6 @@ CRef Solver::reason(Var x) {
     }
     return vardata[x].d_reason;
   }
-
   // What's the literal we are trying to explain
   Lit l = mkLit(x, value(x) != l_True);
 
@@ -428,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() && !isProofEnabled())
+    if (options::unsatCores())
     {
       ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
                                                                 THEORY_LEMMA);
@@ -515,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() && !isProofEnabled())
+      if (options::unsatCores())
       {
         // Store the expression being converted to CNF until
         // the clause is actually created
@@ -534,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() && !isProofEnabled())
+            if (options::unsatCores())
             {
               ClauseKind ck =
                   ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -577,7 +576,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
         if (options::unsatCores() || isProofEnabled())
         {
-          if (options::unsatCores() && !isProofEnabled())
+          if (options::unsatCores())
           {
             ClauseKind ck =
                 ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -593,7 +592,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           if (ps.size() == falseLiteralsCount)
           {
-            if (options::unsatCores() && !isProofEnabled())
+            if (options::unsatCores())
             {
               ProofManager::getSatProof()->finalizeProof(cr);
             }
@@ -615,7 +614,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
                          << std::endl;
           if (ps.size() == 1)
           {
-            if (options::unsatCores() && !isProofEnabled())
+            if (options::unsatCores())
             {
               ClauseKind ck =
                   ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -641,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() && !isProofEnabled())
+            if (options::unsatCores())
             {
               if (ca[confl].size() == 1)
               {
@@ -669,7 +668,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           return ok;
         } else {
-          if (options::unsatCores() && !isProofEnabled())
+          if (options::unsatCores())
           {
             id = ClauseIdUndef;
           }
@@ -716,7 +715,7 @@ void Solver::detachClause(CRef cr, bool strict) {
       Debug("minisat") << "\n";
     }
     Assert(c.size() > 1);
-    if (options::unsatCores() && !isProofEnabled())
+    if (options::unsatCores())
     {
       ProofManager::getSatProof()->markDeleted(cr);
     }
@@ -998,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() && !isProofEnabled())
+  if (options::unsatCores())
   {
     ProofManager::getSatProof()->startResChain(confl);
     }
@@ -1062,7 +1061,7 @@ 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() && !isProofEnabled())
+              if (options::unsatCores())
               {
                 ProofManager::getSatProof()->resolveOutUnit(q);
               }
@@ -1084,7 +1083,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 
         if (pathC > 0 && confl != CRef_Undef)
         {
-          if (options::unsatCores() && !isProofEnabled())
+          if (options::unsatCores())
           {
             ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
           }
@@ -1124,7 +1123,7 @@ 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() && !isProofEnabled())
+                if (options::unsatCores())
                 {
                   ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
                 }
@@ -1420,7 +1419,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() && !isProofEnabled())
+        if (options::unsatCores())
         {
           ProofManager::getCnfProof()->popCurrentAssertion();
         }
@@ -1564,7 +1563,7 @@ 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() && !isProofEnabled() && locked(c))
+          if (options::unsatCores() && locked(c))
           {
             // store a resolution of the literal c propagated
             ProofManager::getSatProof()->storeUnitResolution(c[0]);
@@ -1671,7 +1670,7 @@ lbool Solver::search(int nof_conflicts)
 
       if (decisionLevel() == 0)
       {
-        if (options::unsatCores() && !isProofEnabled())
+        if (options::unsatCores())
         {
           ProofManager::getSatProof()->finalizeProof(confl);
         }
@@ -1698,7 +1697,7 @@ lbool Solver::search(int nof_conflicts)
       if (learnt_clause.size() == 1)
       {
         uncheckedEnqueue(learnt_clause[0]);
-        if (options::unsatCores() && !isProofEnabled())
+        if (options::unsatCores())
         {
           ProofManager::getSatProof()->endResChain(learnt_clause[0]);
         }
@@ -1716,7 +1715,7 @@ lbool Solver::search(int nof_conflicts)
         attachClause(cr);
         claBumpActivity(ca[cr]);
         uncheckedEnqueue(learnt_clause[0], cr);
-        if (options::unsatCores() && !isProofEnabled())
+        if (options::unsatCores())
         {
           ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
           ProofManager::getSatProof()->endResChain(id);
@@ -2059,9 +2058,8 @@ void Solver::relocAll(ClauseAllocator& to)
             {
               ca.reloc(ws[j].cref,
                        to,
-                       (options::unsatCores() && !isProofEnabled())
-                           ? ProofManager::getSatProof()
-                           : nullptr);
+                       options::unsatCores() ? ProofManager::getSatProof()
+                                             : nullptr);
             }
         }
 
@@ -2073,11 +2071,10 @@ void Solver::relocAll(ClauseAllocator& to)
         if (hasReasonClause(v)
             && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
         {
-          ca.reloc(vardata[v].d_reason,
-                   to,
-                   (options::unsatCores() && !isProofEnabled())
-                       ? ProofManager::getSatProof()
-                       : nullptr);
+          ca.reloc(
+              vardata[v].d_reason,
+              to,
+              options::unsatCores() ? ProofManager::getSatProof() : nullptr);
         }
     }
     // All learnt:
@@ -2086,9 +2083,7 @@ void Solver::relocAll(ClauseAllocator& to)
     {
       ca.reloc(clauses_removable[i],
                to,
-               (options::unsatCores() && !isProofEnabled())
-                   ? ProofManager::getSatProof()
-                   : nullptr);
+               options::unsatCores() ? ProofManager::getSatProof() : nullptr);
     }
     // All original:
     //
@@ -2096,11 +2091,9 @@ void Solver::relocAll(ClauseAllocator& to)
     {
       ca.reloc(clauses_persistent[i],
                to,
-               (options::unsatCores() && !isProofEnabled())
-                   ? ProofManager::getSatProof()
-                   : nullptr);
+               options::unsatCores() ? ProofManager::getSatProof() : nullptr);
     }
-    if (options::unsatCores() && !isProofEnabled())
+    if (options::unsatCores())
     {
       ProofManager::getSatProof()->finishUpdateCRef();
     }
@@ -2270,7 +2263,7 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      if (options::unsatCores() && !isProofEnabled())
+      if (options::unsatCores())
       {
         TNode cnf_assertion = lemmas_cnf_assertion[j];
 
@@ -2291,7 +2284,7 @@ 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() && !isProofEnabled() && lemma.size() == 1)
+        if (options::unsatCores() && lemma.size() == 1)
         {
           Node cnf_assertion = lemmas_cnf_assertion[j];
 
@@ -2311,7 +2304,7 @@ CRef Solver::updateLemmas() {
           } else {
             Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
             conflict = CRef_Lazy;
-            if (options::unsatCores() && !isProofEnabled())
+            if (options::unsatCores())
             {
               ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
             }
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index b7d80da76..a15864ad3 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -519,23 +519,33 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn)
   Node proven = trn.getProven();
   Trace("cnf") << "ProofCnfStream::convertPropagation: proven explanation"
                << proven << "\n";
-  Assert(trn.getGenerator());
-  Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
-  Trace("cnf-steps") << proven << " by explainPropagation "
-                     << trn.identifyGenerator() << std::endl;
-  d_proof.addLazyStep(proven,
-                      trn.getGenerator(),
-                      PfRule::ASSUME,
-                      true,
-                      "ProofCnfStream::convertPropagation");
+  // If we are not producing proofs in the theory engine there is no need to
+  // keep track in d_proof of the clausification. We still need however to let
+  // the SAT proof manager know that this clause is an assumption.
+  bool proofLogging = trn.getGenerator() != nullptr;
+  if (proofLogging)
+  {
+    Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
+    Trace("cnf-steps") << proven << " by explainPropagation "
+                       << trn.identifyGenerator() << std::endl;
+    d_proof.addLazyStep(proven,
+                        trn.getGenerator(),
+                        PfRule::ASSUME,
+                        true,
+                        "ProofCnfStream::convertPropagation");
+  }
   // since the propagation is added directly to the SAT solver via theoryProxy,
   // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here
   NodeManager* nm = NodeManager::currentNM();
-  Node clauseImpliesElim = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
-  Trace("cnf") << "ProofCnfStream::convertPropagation: adding "
-               << PfRule::IMPLIES_ELIM << " rule to conclude "
-               << clauseImpliesElim << "\n";
-  d_proof.addStep(clauseImpliesElim, PfRule::IMPLIES_ELIM, {proven}, {});
+  Node clauseImpliesElim;
+  if (proofLogging)
+  {
+    clauseImpliesElim = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
+    Trace("cnf") << "ProofCnfStream::convertPropagation: adding "
+                 << PfRule::IMPLIES_ELIM << " rule to conclude "
+                 << clauseImpliesElim << "\n";
+    d_proof.addStep(clauseImpliesElim, PfRule::IMPLIES_ELIM, {proven}, {});
+  }
   Node clauseExp;
   // need to eliminate AND
   if (proven[0].getKind() == kind::AND)
@@ -548,27 +558,33 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn)
       disjunctsRes.push_back(proven[0][i].notNode());
     }
     disjunctsRes.push_back(proven[1]);
-    Node clauseAndNeg = nm->mkNode(kind::OR, disjunctsAndNeg);
-    // add proof steps to convert into clause
-    d_proof.addStep(clauseAndNeg, PfRule::CNF_AND_NEG, {}, {proven[0]});
     clauseExp = nm->mkNode(kind::OR, disjunctsRes);
-    d_proof.addStep(clauseExp,
-                    PfRule::RESOLUTION,
-                    {clauseAndNeg, clauseImpliesElim},
-                    {nm->mkConst(true), proven[0]});
+    if (proofLogging)
+    {
+      // add proof steps to convert into clause
+      Node clauseAndNeg = nm->mkNode(kind::OR, disjunctsAndNeg);
+      d_proof.addStep(clauseAndNeg, PfRule::CNF_AND_NEG, {}, {proven[0]});
+      d_proof.addStep(clauseExp,
+                      PfRule::RESOLUTION,
+                      {clauseAndNeg, clauseImpliesElim},
+                      {nm->mkConst(true), proven[0]});
+    }
   }
   else
   {
-    clauseExp = clauseImpliesElim;
+    clauseExp = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
   }
   normalizeAndRegister(clauseExp);
   // consume steps
-  const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
-  for (const std::pair<Node, ProofStep>& step : steps)
+  if (proofLogging)
   {
-    d_proof.addStep(step.first, step.second);
+    const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
+    for (const std::pair<Node, ProofStep>& step : steps)
+    {
+      d_proof.addStep(step.first, step.second);
+    }
+    d_psb.clear();
   }
-  d_psb.clear();
 }
 
 void ProofCnfStream::ensureLiteral(TNode n)
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index d696db580..6299471dd 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -79,12 +79,11 @@ class ProofCnfStream : public ProofGenerator
                         ProofGenerator* pg);
 
   /**
-   * Clausifies the given propagation lemma *without* registering the
-   * resoluting clause in the SAT solver, as this is handled internally by the
-   * SAT solver. The clausification steps and the generator within the trust
-   * node are saved in d_proof. */
+   * Clausifies the given propagation lemma *without* registering the resoluting
+   * clause in the SAT solver, as this is handled internally by the SAT
+   * solver. The clausification steps and the generator within the trust node
+   * are saved in d_proof if we are producing proofs in the theory engine. */
   void convertPropagation(theory::TrustNode ttn);
-
   /**
    * Ensure that the given node will have a designated SAT literal that is
    * definitionally equal to it.  The result of this function is that the Node
@@ -152,6 +151,7 @@ class ProofCnfStream : public ProofGenerator
    * above normalizations on all added clauses.
    */
   void normalizeAndRegister(TNode clauseNode);
+
   /** Reference to the underlying cnf stream. */
   CnfStream& d_cnfStream;
   /** The proof manager of underlying SAT solver associated with this stream. */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 4af943537..2eaa3a812 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -246,7 +246,8 @@ 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);
+  Assert(!isProofEnabled() || trn.getGenerator() != nullptr
+         || options::unsatCores() || options::unsatCoresNew());
   assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
 }
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index bf386fc0e..6ff2af527 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -96,8 +96,9 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
   theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
-  if (cvc5::options::produceProofs())
+  if (options::produceProofs())
   {
+    Assert(options::unsatCoresNew() || tte.getGenerator());
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }
   else if (options::unsatCores())
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index d873f31bb..aee7a2a86 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() && !isProofEnabled())
+  if (options::unsatCores())
   {
     if (inInput)
     {  // n is an input assertion
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";
 }
 
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 0345991d2..253dbecaf 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -38,6 +38,24 @@ class ProofPostproccess;
 /**
  * This class is responsible for managing the proof output of SmtEngine, as
  * well as setting up the global proof checker and proof node manager.
+ *
+ * The proof production of an SmtEngine is directly impacted by whether, and
+ * how, we are producing unsat cores:
+ *
+ * - If we are producing unsat cores using the old proof infrastructure, then
+ *   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.
+ *
+ * - If we are not producing unsat cores then the SmtEngine will have proofs as
+ *   long as --produce-proofs was given.
+ *
+ * - If SmtEngine has been configured in a way that is incompatible with proofs
+ *   then unsat core production will be disabled.
  */
 class PfManager
 {
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 0a8819c4b..cf5fc267b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -70,13 +70,36 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Notice() << "SmtEngine: setting dumpUnsatCores" << std::endl;
     options::dumpUnsatCores.set(true);
   }
-  if (options::checkUnsatCores() || options::checkUnsatCoresNew()
-      || options::dumpUnsatCores() || options::unsatAssumptions())
+  if ((options::unsatCores() && options::unsatCoresNew())
+      || (options::checkUnsatCores() && options::checkUnsatCoresNew()))
+  {
+    AlwaysAssert(false) << "Can't have both unsat cores modes, pick one.\n";
+  }
+  if (options::checkUnsatCores())
   {
-    Notice() << "SmtEngine: setting unsatCores" << std::endl;
     options::unsatCores.set(true);
   }
-  if (options::checkProofs() || options::checkUnsatCoresNew()
+  if (options::checkUnsatCoresNew())
+  {
+    options::unsatCoresNew.set(true);
+  }
+  if (options::dumpUnsatCores() || options::unsatAssumptions())
+  {
+    if (!options::unsatCoresNew())
+    {
+      Notice() << "SmtEngine: setting unsatCores" << std::endl;
+      options::unsatCores.set(true);
+    }
+  }
+  if (options::unsatCoresNew()
+      && ((options::produceProofs() && options::produceProofs.wasSetByUser())
+          || (options::checkProofs() && options::checkProofs.wasSetByUser())
+          || (options::dumpProofs() && options::dumpProofs.wasSetByUser())))
+  {
+    AlwaysAssert(false) << "Can't properly produce proofs and have the new "
+                           "unsat cores simultaneously.\n";
+  }
+  if (options::checkProofs() || options::unsatCoresNew()
       || options::dumpProofs())
   {
     Notice() << "SmtEngine: setting proof" << std::endl;
@@ -278,11 +301,21 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   // !!! must disable proofs if using the old unsat core infrastructure
   // TODO (#project 37) remove this
-  if (options::unsatCores() && !options::checkUnsatCoresNew())
+  if (options::unsatCores())
   {
     disableProofs = true;
   }
 
+  // new unsat core specific restrictions for proofs
+  if (options::unsatCoresNew())
+  {
+    // no fine-graininess
+    if (!options::proofGranularityMode.wasSetByUser())
+    {
+      options::proofGranularityMode.set(options::ProofGranularityMode::OFF);
+    }
+  }
+
   if (options::arraysExp())
   {
     if (!logic.isQuantified())
@@ -335,6 +368,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // if we requiring disabling proofs, disable them now
   if (disableProofs && options::produceProofs())
   {
+    if (options::unsatCoresNew())
+    {
+      Notice() << "SmtEngine: turning off new unsat cores." << std::endl;
+    }
+    options::unsatCoresNew.set(false);
+    options::checkUnsatCoresNew.set(false);
     if (options::produceProofs())
     {
       Notice() << "SmtEngine: turning off produce-proofs." << std::endl;
@@ -366,7 +405,8 @@ 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())
+  if (options::incrementalSolving() || options::unsatCores()
+      || options::unsatCoresNew())
   {
     if (options::unconstrainedSimp())
     {
@@ -428,7 +468,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   // Disable options incompatible with unsat cores or output an error if enabled
   // explicitly
-  if (options::unsatCores())
+  if (options::unsatCores() || options::unsatCoresNew())
   {
     if (options::simplificationMode() != options::SimplificationMode::NONE)
     {
@@ -707,7 +747,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
                        && !options::incrementalSolving()
-                       && !options::unsatCores();
+                       && !options::unsatCores() && !options::unsatCoresNew();
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
                  << std::endl;
     options::ufSymmetryBreaker.set(qf_uf_noinc);
@@ -756,7 +796,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                       && (logic.isTheoryEnabled(THEORY_ARRAYS)
                           && logic.isTheoryEnabled(THEORY_UF)
                           && logic.isTheoryEnabled(THEORY_BV))
-                      && !options::unsatCores();
+                      && !options::unsatCores() && !options::unsatCoresNew();
     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 3eedfdf53..3d38ba37b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -236,7 +236,10 @@ void SmtEngine::finishInit()
   }
 
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
-  d_smtSolver->finishInit(logic);
+  // 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());
 
   // now can construct the SMT-level model object
   TheoryEngine* te = d_smtSolver->getTheoryEngine();
@@ -1408,10 +1411,11 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry()
 
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
-  if (!options::unsatCores())
+  if (!options::unsatCores() && !options::unsatCoresNew())
   {
     throw ModalException(
-        "Cannot get an unsat core when produce-unsat-cores option is off.");
+        "Cannot get an unsat core when produce-unsat-cores[-new] option is "
+        "off.");
   }
   if (d_state->getMode() != SmtMode::UNSAT)
   {
@@ -1437,7 +1441,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
 }
 
 void SmtEngine::checkUnsatCore() {
-  Assert(options::unsatCores())
+  Assert(options::unsatCores() || options::unsatCoresNew())
       << "cannot check unsat core if unsat cores are turned off";
 
   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
@@ -1449,7 +1453,10 @@ void SmtEngine::checkUnsatCore() {
   coreChecker->getOptions().set(options::checkUnsatCores, false);
   // 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
   TypeNode sepLocType, sepDataType;
   if (getSepHeapTypes(sepLocType, sepDataType))
@@ -1633,7 +1640,8 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (options::produceProofs() && getSmtMode() == SmtMode::UNSAT)
+  if (options::produceProofs() && !options::unsatCoresNew()
+      && getSmtMode() == SmtMode::UNSAT)
   {
     // minimize instantiations based on proof manager
     getRelevantInstantiationTermVectors(insts);
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index ceec0619b..2847e5ee9 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -49,16 +49,18 @@ SmtSolver::SmtSolver(SmtEngine& smt,
 
 SmtSolver::~SmtSolver() {}
 
-void SmtSolver::finishInit(const LogicInfo& logicInfo)
+void SmtSolver::finishInit(const LogicInfo& logicInfo,
+                           bool proofForUnsatCoreMode)
 {
   // 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(),
-                                        d_pnm));
+  d_theoryEngine.reset(
+      new TheoryEngine(d_smt.getContext(),
+                       d_smt.getUserContext(),
+                       d_rm,
+                       logicInfo,
+                       d_smt.getOutputManager(),
+                       proofForUnsatCoreMode ? 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 e4493eedf..ae1cc2e40 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -71,8 +71,13 @@ class SmtSolver
   ~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);
+  void finishInit(const LogicInfo& logicInfo,
+                  bool proofForUnsatCoreMode = false);
   /** Reset all assertions, global declarations, etc.  */
   void resetAssertions();
   /**
@@ -129,6 +134,7 @@ class SmtSolver
   /** Get a pointer to the preprocessor */
   Preprocessor* getPreprocessor();
   //------------------------------------------ end access methods
+
  private:
   /** Reference to the parent SMT engine */
   SmtEngine& d_smt;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9f0e3eb82..79f9c660f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1784,7 +1784,7 @@ theory::TrustNode TheoryEngine::getExplanation(
     return trn;
   }
 
-  return theory::TrustNode::mkTrustLemma(expNode, nullptr);
+  return theory::TrustNode::mkTrustPropExp(conclusion, expNode, nullptr);
 }
 
 bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }