Removes old proof code (#4964)

This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.

It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).

5 files changed, 292 insertions, 189 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index f56f6a447..311224a03 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -30,6 +30,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "options/prop_options.h"
 #include "options/smt_options.h"
 #include "proof/clause_id.h"
+#include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
 #include "proof/sat_proof_implementation.h"
@@ -217,7 +218,10 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy,
       propagation_budget(-1),
       asynch_interrupt(false)
 {
-  PROOF(ProofManager::currentPM()->initSatProof(this);)
+  if (options::unsatCores())
+  {
+    ProofManager::currentPM()->initSatProof(this);
+  }
 
   // Create the constant variables
   varTrue = newVar(true, false, false);
@@ -227,11 +231,11 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy,
   uncheckedEnqueue(mkLit(varTrue, false));
   uncheckedEnqueue(mkLit(varFalse, true));
   // FIXME: these should be axioms I believe
-  PROOF
-    (
-     ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
-     ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
-     );
+  if (options::unsatCores())
+  {
+    ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
+    ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
+  }
 }
 
 
@@ -390,15 +394,20 @@ CRef Solver::reason(Var x) {
     // FIXME: at some point will need more information about where this explanation
     // came from (ie. the theory/sharing)
     Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
-    PROOF(ClauseId id = ProofManager::getSatProof()->registerClause(
-              real_reason, THEORY_LEMMA);
-          ProofManager::getCnfProof()->registerConvertedClause(id, true);
-          // explainPropagation() pushes the explanation on the assertion stack
-          // in CnfProof, so we need to pop it here. This is important because
-          // reason() may be called indirectly while adding a clause, which can
-          // lead to a wrong assertion being associated with the clause being
-          // added (see issue #2137).
-          ProofManager::getCnfProof()->popCurrentAssertion(););
+    if (options::unsatCores())
+    {
+      ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
+                                                                THEORY_LEMMA);
+      // map id to assertion, which may be required if looking for
+      // lemmas in unsat core
+      ProofManager::getCnfProof()->registerConvertedClause(id);
+      // explainPropagation() pushes the explanation on the assertion stack
+      // in CnfProof, so we need to pop it here. This is important because
+      // reason() may be called indirectly while adding a clause, which can
+      // lead to a wrong assertion being associated with the clause being
+      // added (see issue #2137).
+      ProofManager::getCnfProof()->popCurrentAssertion();
+    }
     vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
     clauses_removable.push(real_reason);
     attachClause(real_reason);
@@ -441,9 +450,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
       }
       // If a literal is false at 0 level (both sat and user level) we also ignore it
       if (value(ps[i]) == l_False) {
-        if (!PROOF_ON() && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
+        if (!options::unsatCores() && level(var(ps[i])) == 0
+            && user_level(var(ps[i])) == 0)
+        {
           continue;
-        } else {
+        }
+        else
+        {
           // If we decide to keep it, we count it into the false literals
           falseLiteralsCount ++;
         }
@@ -467,34 +480,46 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
       lemmas.push();
       ps.copyTo(lemmas.last());
       lemmas_removable.push(removable);
-      PROOF(
-            // Store the expression being converted to CNF until
-            // the clause is actually created
-            Node assertion = ProofManager::getCnfProof()->getCurrentAssertion();
-            Node def = ProofManager::getCnfProof()->getCurrentDefinition();
-            lemmas_cnf_assertion.push_back(std::make_pair(assertion, def));
-            id = ClauseIdUndef;
-        );
-      // does it have to always be a lemma?
-      // PROOF(id = ProofManager::getSatProof()->registerUnitClause(ps[0], THEORY_LEMMA););
-      // PROOF(id = ProofManager::getSatProof()->registerTheoryLemma(ps););
-      // Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
-      // lemmas_proof_id.push(proof_id);
+      if (options::unsatCores())
+      {
+        // Store the expression being converted to CNF until
+        // the clause is actually created
+        lemmas_cnf_assertion.push_back(
+            ProofManager::getCnfProof()->getCurrentAssertion());
+        id = ClauseIdUndef;
+      }
     } else {
       assert(decisionLevel() == 0);
 
       // If all false, we're in conflict
       if (ps.size() == falseLiteralsCount) {
-        if(PROOF_ON()) {
+        if (options::unsatCores())
+        {
           // Take care of false units here; otherwise, we need to
           // construct the clause below to give to the proof manager
           // as the final conflict.
           if(falseLiteralsCount == 1) {
-            PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); )
-            PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); )
+            if (options::unsatCores())
+            {
+              ClauseKind ck =
+                  ProofManager::getCnfProof()->getCurrentAssertionKind()
+                      ? INPUT
+                      : THEORY_LEMMA;
+              id = ProofManager::getSatProof()->storeUnitConflict(ps[0], ck);
+              // map id to assertion, which may be required if looking for
+              // lemmas in unsat core
+              if (ck == THEORY_LEMMA)
+              {
+                ProofManager::getCnfProof()->registerConvertedClause(id);
+              }
+              ProofManager::getSatProof()->finalizeProof(
+                  CVC4::Minisat::CRef_Lazy);
+            }
             return ok = false;
           }
-        } else {
+        }
+        else
+        {
           return ok = false;
         }
       }
@@ -509,14 +534,23 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
         cr = ca.alloc(clauseLevel, ps, false);
         clauses_persistent.push(cr);
-	attachClause(cr);
-
-        if(PROOF_ON()) {
-          PROOF(
-                id = ProofManager::getSatProof()->registerClause(cr, INPUT);
-                )
-          if(ps.size() == falseLiteralsCount) {
-            PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
+        attachClause(cr);
+
+        if (options::unsatCores())
+        {
+          ClauseKind ck = ProofManager::getCnfProof()->getCurrentAssertionKind()
+                              ? INPUT
+                              : THEORY_LEMMA;
+          id = ProofManager::getSatProof()->registerClause(cr, ck);
+          // map id to assertion, which may be required if looking for
+          // lemmas in unsat core
+          if (ck == THEORY_LEMMA)
+          {
+            ProofManager::getCnfProof()->registerConvertedClause(id);
+          }
+          if (ps.size() == falseLiteralsCount)
+          {
+            ProofManager::getSatProof()->finalizeProof(cr);
             return ok = false;
           }
         }
@@ -527,15 +561,25 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
         if(assigns[var(ps[0])] == l_Undef) {
           assert(assigns[var(ps[0])] != l_False);
           uncheckedEnqueue(ps[0], cr);
-          Debug("cores") << "i'm registering a unit clause, input" << std::endl;
-          PROOF(
-                if(ps.size() == 1) {
-                  id = ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT);
-                }
-                );
+          Debug("cores") << "i'm registering a unit clause, maybe input"
+                         << std::endl;
+          if (options::unsatCores() && ps.size() == 1)
+          {
+            ClauseKind ck =
+                ProofManager::getCnfProof()->getCurrentAssertionKind()
+                    ? INPUT
+                    : THEORY_LEMMA;
+            id = ProofManager::getSatProof()->registerUnitClause(ps[0], ck);
+            // map id to assertion, which may be required if looking for
+            // lemmas in unsat core
+            if (ck == THEORY_LEMMA)
+            {
+              ProofManager::getCnfProof()->registerConvertedClause(id);
+            }
+          }
           CRef confl = propagate(CHECK_WITHOUT_THEORY);
           if(! (ok = (confl == CRef_Undef)) ) {
-            if (PROOF_ON())
+            if (options::unsatCores())
             {
               if (ca[confl].size() == 1)
               {
@@ -552,7 +596,10 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           return ok;
         } else {
-          PROOF(id = ClauseIdUndef;);
+          if (options::unsatCores())
+          {
+            id = ClauseIdUndef;
+          }
           return ok;
         }
       }
@@ -575,7 +622,10 @@ void Solver::attachClause(CRef cr) {
 
 void Solver::detachClause(CRef cr, bool strict) {
     const Clause& c = ca[cr];
-    PROOF( ProofManager::getSatProof()->markDeleted(cr); );
+    if (options::unsatCores())
+    {
+      ProofManager::getSatProof()->markDeleted(cr);
+    }
     Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
     assert(c.size() > 1);
 
@@ -826,7 +876,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 
     int max_resolution_level = 0; // Maximal level of the resolved clauses
 
-    PROOF( ProofManager::getSatProof()->startResChain(confl); )
+    if (options::unsatCores())
+    {
+      ProofManager::getSatProof()->startResChain(confl);
+    }
     do{
         assert(confl != CRef_Undef); // (otherwise should be UIP)
 
@@ -867,9 +920,9 @@ 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() && level(var(q)) == 0)
             {
-              PROOF(ProofManager::getSatProof()->resolveOutUnit(q);)
+              ProofManager::getSatProof()->resolveOutUnit(q);
             }
           }
         }
@@ -881,8 +934,9 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
         seen[var(p)] = 0;
         pathC--;
 
-        if ( pathC > 0 && confl != CRef_Undef ) {
-          PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); )
+        if (options::unsatCores() && pathC > 0 && confl != CRef_Undef)
+        {
+          ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
         }
 
     }while (pathC > 0);
@@ -905,7 +959,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                 // Literal is not redundant
                 out_learnt[j++] = out_learnt[i];
               } else {
-                PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); )
+                if (options::unsatCores())
+                {
+                  ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
+                }
                 // Literal is redundant, to be safe, mark the level as current assertion level
                 // TODO: maybe optimize
                 max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i])));
@@ -1169,7 +1226,10 @@ void Solver::propagateTheory() {
         addClause(explanation, true, id);
         // explainPropagation() pushes the explanation on the assertion
         // stack in CnfProof, so we need to pop it here.
-        PROOF(ProofManager::getCnfProof()->popCurrentAssertion();)
+        if (options::unsatCores())
+        {
+          ProofManager::getCnfProof()->popCurrentAssertion();
+        }
       }
     }
   }
@@ -1310,9 +1370,10 @@ void Solver::removeSatisfied(vec<CRef>& cs)
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
         if (satisfied(c)) {
-          if (locked(c)) {
+          if (options::unsatCores() && locked(c))
+          {
             // store a resolution of the literal c propagated
-            PROOF( ProofManager::getSatProof()->storeUnitResolution(c[0]); )
+            ProofManager::getSatProof()->storeUnitResolution(c[0]);
           }
             removeClause(cs[i]);
         }
@@ -1412,8 +1473,11 @@ lbool Solver::search(int nof_conflicts)
             conflicts++; conflictC++;
 
             if (decisionLevel() == 0) {
-                PROOF( ProofManager::getSatProof()->finalizeProof(confl); )
-                return l_False;
+              if (options::unsatCores())
+              {
+                ProofManager::getSatProof()->finalizeProof(confl);
+              }
+              return l_False;
             }
 
             // Analyze the conflict
@@ -1425,8 +1489,10 @@ lbool Solver::search(int nof_conflicts)
             if (learnt_clause.size() == 1) {
                 uncheckedEnqueue(learnt_clause[0]);
 
-                PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); )
-
+                if (options::unsatCores())
+                {
+                  ProofManager::getSatProof()->endResChain(learnt_clause[0]);
+                }
             } else {
               CRef cr =
                   ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
@@ -1436,15 +1502,12 @@ lbool Solver::search(int nof_conflicts)
               attachClause(cr);
               claBumpActivity(ca[cr]);
               uncheckedEnqueue(learnt_clause[0], cr);
-              PROOF(ClauseId id =
-                        ProofManager::getSatProof()->registerClause(cr, LEARNT);
-                    PSTATS(std::unordered_set<int> cl_levels;
-                           for (int i = 0; i < learnt_clause.size(); ++i) {
-                             cl_levels.insert(level(var(learnt_clause[i])));
-                           } ProofManager::getSatProof()
-                               ->storeClauseGlue(id, cl_levels.size());)
-                        ProofManager::getSatProof()
-                            ->endResChain(id););
+              if (options::unsatCores())
+              {
+                ClauseId id =
+                    ProofManager::getSatProof()->registerClause(cr, LEARNT);
+                ProofManager::getSatProof()->endResChain(id);
+              }
             }
 
             varDecayActivity();
@@ -1469,25 +1532,33 @@ lbool Solver::search(int nof_conflicts)
             }
 
         } else {
-
-	    // If this was a final check, we are satisfiable
-            if (check_type == CHECK_FINAL) {
-              bool decisionEngineDone = d_proxy->isDecisionEngineDone();
-              // Unless a lemma has added more stuff to the queues
-              if (!decisionEngineDone  &&
-		  (!order_heap.empty() || qhead < trail.size()) ) {
-                check_type = CHECK_WITH_THEORY;
-                continue;
-              } else if (recheck) {
-                // There some additional stuff added, so we go for another full-check
-                continue;
-              } else {
-                // Yes, we're truly satisfiable
-                return l_True;
-              }
-            } else if (check_type == CHECK_FINAL_FAKE) {
+          // If this was a final check, we are satisfiable
+          if (check_type == CHECK_FINAL)
+          {
+            bool decisionEngineDone = d_proxy->isDecisionEngineDone();
+            // Unless a lemma has added more stuff to the queues
+            if (!decisionEngineDone
+                && (!order_heap.empty() || qhead < trail.size()))
+            {
               check_type = CHECK_WITH_THEORY;
+              continue;
+            }
+            else if (recheck)
+            {
+              // There some additional stuff added, so we go for another
+              // full-check
+              continue;
             }
+            else
+            {
+              // Yes, we're truly satisfiable
+              return l_True;
+            }
+          }
+          else if (check_type == CHECK_FINAL_FAKE)
+          {
+            check_type = CHECK_WITH_THEORY;
+          }
 
             if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
                 || !withinBudget(ResourceManager::Resource::SatConflictStep))
@@ -1744,7 +1815,10 @@ void Solver::relocAll(ClauseAllocator& to)
             // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
             vec<Watcher>& ws = watches[p];
             for (int j = 0; j < ws.size(); j++)
-              ca.reloc(ws[j].cref, to, NULLPROOF(ProofManager::getSatProof()));
+              ca.reloc(ws[j].cref,
+                       to,
+                       CVC4::options::unsatCores() ? ProofManager::getSatProof()
+                                                   : nullptr);
         }
 
     // All reasons:
@@ -1753,22 +1827,31 @@ void Solver::relocAll(ClauseAllocator& to)
         Var v = var(trail[i]);
 
         if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
-          ca.reloc(
-              vardata[v].d_reason, to, NULLPROOF(ProofManager::getSatProof()));
+          ca.reloc(vardata[v].d_reason,
+                   to,
+                   CVC4::options::unsatCores() ? ProofManager::getSatProof()
+                                               : nullptr);
     }
     // All learnt:
     //
     for (int i = 0; i < clauses_removable.size(); i++)
       ca.reloc(
-          clauses_removable[i], to, NULLPROOF(ProofManager::getSatProof()));
+          clauses_removable[i],
+          to,
+          CVC4::options::unsatCores() ? ProofManager::getSatProof() : nullptr);
 
     // All original:
     //
     for (int i = 0; i < clauses_persistent.size(); i++)
       ca.reloc(
-          clauses_persistent[i], to, NULLPROOF(ProofManager::getSatProof()));
+          clauses_persistent[i],
+          to,
+          CVC4::options::unsatCores() ? ProofManager::getSatProof() : nullptr);
 
-    PROOF(ProofManager::getSatProof()->finishUpdateCRef();)
+    if (options::unsatCores())
+    {
+      ProofManager::getSatProof()->finishUpdateCRef();
+    }
 }
 
 
@@ -1874,7 +1957,7 @@ CRef Solver::updateLemmas() {
 
       // If it's an empty lemma, we have a conflict at zero level
       if (lemma.size() == 0) {
-        Assert(!PROOF_ON());
+        Assert(!options::unsatCores());
         conflict = CRef_Lazy;
         backtrackLevel = 0;
         Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -1904,7 +1987,8 @@ CRef Solver::updateLemmas() {
   // Last index in the trail
   int backtrack_index = trail.size();
 
-  PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
+  Assert(!options::unsatCores()
+         || lemmas.size() == (int)lemmas_cnf_assertion.size());
 
   // Attach all the clauses and enqueue all the propagations
   for (int j = 0; j < lemmas.size(); ++j)
@@ -1928,15 +2012,16 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      PROOF(TNode cnf_assertion = lemmas_cnf_assertion[j].first;
-            TNode cnf_def = lemmas_cnf_assertion[j].second;
-
-            Debug("pf::sat")
-            << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
-            ClauseId id = ProofManager::getSatProof()->registerClause(
-                lemma_ref, THEORY_LEMMA);
-            ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
-            ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def););
+      if (options::unsatCores())
+      {
+        TNode cnf_assertion = lemmas_cnf_assertion[j];
+
+        Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)"
+                         << std::endl;
+        ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref,
+                                                                  THEORY_LEMMA);
+        ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+      }
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {
@@ -1948,17 +2033,15 @@ 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 (PROOF_ON() && lemma.size() == 1)
+        if (options::unsatCores() && lemma.size() == 1)
         {
-          Node cnf_assertion = lemmas_cnf_assertion[j].first;
-          Node cnf_def = lemmas_cnf_assertion[j].second;
+          Node cnf_assertion = lemmas_cnf_assertion[j];
 
           Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) "
                            << cnf_assertion << value(lemma[0]) << std::endl;
           ClauseId id = ProofManager::getSatProof()->registerUnitClause(
               lemma[0], THEORY_LEMMA);
           ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
-          ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
         }
 
         if (value(lemma[0]) == l_False) {
@@ -1969,7 +2052,10 @@ CRef Solver::updateLemmas() {
           } else {
             Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
             conflict = CRef_Lazy;
-            PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); );
+            if (options::unsatCores())
+            {
+              ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
+            }
           }
         } else {
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
@@ -1979,7 +2065,8 @@ CRef Solver::updateLemmas() {
     }
   }
 
-  PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
+  Assert(!options::unsatCores()
+         || lemmas.size() == (int)lemmas_cnf_assertion.size());
   // Clear the lemmas
   lemmas.clear();
   lemmas_cnf_assertion.clear();
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 508947456..a5f3664e8 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -63,7 +63,7 @@ public:
 
   typedef Var TVar;
   typedef Lit TLit;
-  typedef Clause TClause; 
+  typedef Clause TClause;
   typedef CRef TCRef;
   typedef vec<Lit> TLitVec;
 
@@ -98,7 +98,7 @@ public:
   vec<bool> lemmas_removable;
 
   /** Nodes being converted to CNF */
-  std::vector<std::pair<CVC4::Node, CVC4::Node> > lemmas_cnf_assertion;
+  std::vector<CVC4::Node> lemmas_cnf_assertion;
 
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
@@ -203,7 +203,7 @@ public:
     lbool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
     bool    okay         () const;                  // FALSE means solver is in a conflicting state
 
-    void    toDimacs     (); 
+    void toDimacs();
     void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
     void    toDimacs     (const char *file, const vec<Lit>& assumps);
     void    toDimacs     (FILE* f, Clause& c, vec<Var>& map, Var& max);
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index bbd6e17a2..b30d97aee 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -73,9 +73,14 @@ inline  bool sign      (Lit p)              { return p.x & 1; }
 inline  int  var       (Lit p)              { return p.x >> 1; }
 
 // Mapping Literals to and from compact integers suitable for array indexing:
-inline  int  toInt     (Var v)              { return v; } 
-inline  int  toInt     (Lit p)              { return p.x; } 
-inline  Lit  toLit     (int i)              { Lit p; p.x = i; return p; } 
+inline int toInt(Var v) { return v; }
+inline int toInt(Lit p) { return p.x; }
+inline Lit toLit(int i)
+{
+  Lit p;
+  p.x = i;
+  return p;
+}
 
 //const Lit lit_Undef = mkLit(var_Undef, false);  // }- Useful special constants.
 //const Lit lit_Error = mkLit(var_Undef, true );  // }
@@ -83,20 +88,19 @@ inline  Lit  toLit     (int i)              { Lit p; p.x = i; return p; }
 const Lit lit_Undef = { -2 };  // }- Useful special constants.
 const Lit lit_Error = { -1 };  // }
 
-
 //=================================================================================================
 // Lifted booleans:
 //
-// NOTE: this implementation is optimized for the case when comparisons between values are mostly
-//       between one variable and one constant. Some care had to be taken to make sure that gcc 
-//       does enough constant propagation to produce sensible code, and this appears to be somewhat
-//       fragile unfortunately.
+// NOTE: this implementation is optimized for the case when comparisons between
+// values are mostly
+//       between one variable and one constant. Some care had to be taken to
+//       make sure that gcc does enough constant propagation to produce sensible
+//       code, and this appears to be somewhat fragile unfortunately.
 
 /*
-  This is to avoid multiple definitions of l_True, l_False and l_Undef if using multiple copies of
-  Minisat.
-  IMPORTANT: if we you change the value of the constants so that it is not the same in all copies
-  of Minisat this breaks! 
+  This is to avoid multiple definitions of l_True, l_False and l_Undef if using
+  multiple copies of Minisat. IMPORTANT: if we you change the value of the
+  constants so that it is not the same in all copies of Minisat this breaks!
  */
 
 #ifndef l_True
@@ -124,10 +128,12 @@ public:
     bool  operator != (lbool b) const { return !(*this == b); }
     lbool operator ^  (bool  b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
 
-    lbool operator && (lbool b) const { 
-        uint8_t sel = (this->value << 1) | (b.value << 3);
-        uint8_t v   = (0xF7F755F4 >> sel) & 3;
-        return lbool(v); }
+    lbool operator&&(lbool b) const
+    {
+      uint8_t sel = (this->value << 1) | (b.value << 3);
+      uint8_t v = (0xF7F755F4 >> sel) & 3;
+      return lbool(v);
+    }
 
     lbool operator || (lbool b) const {
         uint8_t sel = (this->value << 1) | (b.value << 3);
@@ -163,7 +169,7 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::vec<Minisat::Lit>&
 }
 
 inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
-  std::string val_str; 
+  std::string val_str;
   if( val == l_False ) {
     val_str = "0";
   } else if (val == l_True ) {
@@ -208,14 +214,14 @@ class Clause {
         header.size      = ps.size();
         header.level     = level;
 
-        for (int i = 0; i < ps.size(); i++) 
-            data[i].lit = ps[i];
+        for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i];
 
         if (header.has_extra){
             if (header.removable)
-                data[header.size].act = 0; 
-            else 
-                calcAbstraction(); }
+              data[header.size].act = 0;
+            else
+              calcAbstraction();
+        }
     }
 
 public:
@@ -321,7 +327,7 @@ class OccLists
 
  public:
     OccLists(const Deleted& d) : deleted(d) {}
-    
+
     void  init      (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
     void  resizeTo  (const Idx& idx);
     // Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }
@@ -394,13 +400,12 @@ class CMap
 
     typedef Map<CRef, T, CRefHash> HashTable;
     HashTable map;
-        
+
  public:
     // Size-operations:
     void     clear       ()                           { map.clear(); }
     int      size        ()                const      { return map.elems(); }
 
-    
     // Insert/Remove/Test mapping:
     void     insert      (CRef cr, const T& t){ map.insert(cr, t); }
     void     growTo      (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
@@ -423,15 +428,14 @@ class CMap
         printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
 };
 
-
 /*_________________________________________________________________________________________________
 |
 |  subsumes : (other : const Clause&)  ->  Lit
-|  
+|
 |  Description:
-|       Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
-|       by subsumption resolution.
-|  
+|       Checks if clause subsumes 'other', and at the same time, if it can be
+used to simplify 'other' |       by subsumption resolution.
+|
 |    Result:
 |       lit_Error  - No subsumption or simplification
 |       lit_Undef  - Clause subsumes 'other'
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index a4d2dce8a..25353e416 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -154,7 +154,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
     return ClauseIdUndef;
   }
   d_minisat->addClause(minisat_clause, removable, clause_id);
-  PROOF(Assert(clause_id != ClauseIdError););
+  Assert(!CVC4::options::unsatCores() || clause_id != ClauseIdError);
   return clause_id;
 }
 
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 23f97b5d5..0ec8981ca 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/simp/SimpSolver.h"
 
 #include "options/prop_options.h"
+#include "options/smt_options.h"
 #include "proof/clause_id.h"
-#include "proof/proof.h"
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/minisat/utils/System.h"
 
@@ -47,25 +47,30 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 //=================================================================================================
 // Constructor/Destructor:
 
-
-SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental) :
-    Solver(proxy, context, enableIncremental)
-  , grow               (opt_grow)
-  , clause_lim         (opt_clause_lim)
-  , subsumption_lim    (opt_subsumption_lim)
-  , simp_garbage_frac  (opt_simp_garbage_frac)
-  , use_asymm          (opt_use_asymm)
-  , use_rcheck         (opt_use_rcheck)
-  , use_elim           (options::minisatUseElim() && !enableIncremental)
-  , merges             (0)
-  , asymm_lits         (0)
-  , eliminated_vars    (0)
-  , elimorder          (1)
-  , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially
-  , occurs             (ClauseDeleted(ca))
-  , elim_heap          (ElimLt(n_occ))
-  , bwdsub_assigns     (0)
-  , n_touched          (0)
+SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy,
+                       CVC4::context::Context* context,
+                       bool enableIncremental)
+    : Solver(proxy, context, enableIncremental),
+      grow(opt_grow),
+      clause_lim(opt_clause_lim),
+      subsumption_lim(opt_subsumption_lim),
+      simp_garbage_frac(opt_simp_garbage_frac),
+      use_asymm(opt_use_asymm),
+      use_rcheck(opt_use_rcheck),
+      use_elim(options::minisatUseElim() && !enableIncremental),
+      merges(0),
+      asymm_lits(0),
+      eliminated_vars(0),
+      elimorder(1),
+      use_simplification(
+          !enableIncremental
+          && !options::unsatCores())  // TODO: turn off simplifications if
+                                      // proofs are on initially
+      ,
+      occurs(ClauseDeleted(ca)),
+      elim_heap(ElimLt(n_occ)),
+      bwdsub_assigns(0),
+      n_touched(0)
 {
     if(options::minisatUseElim() &&
        options::minisatUseElim.wasSetByUser() &&
@@ -117,8 +122,8 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister
 lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 {
     if (options::minisatDumpDimacs()) {
-      toDimacs(); 
-      return l_Undef; 
+      toDimacs();
+      return l_Undef;
     }
     assert(decisionLevel() == 0);
 
@@ -533,9 +538,10 @@ bool SimpSolver::eliminateVar(Var v)
 
     for (int i = 0; i < pos.size(); i++)
         for (int j = 0; j < neg.size(); j++)
-            if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) && 
-                (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
-                return true;
+          if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
+              && (++cnt > cls.size() + grow
+                  || (clause_lim != -1 && clause_size > clause_lim)))
+            return true;
 
     // Delete and store old clauses:
     eliminated[v] = true;
@@ -552,10 +558,9 @@ bool SimpSolver::eliminateVar(Var v)
         mkElimClause(elimclauses, ~mkLit(v));
     }
 
-    for (int i = 0; i < cls.size(); i++)
-        removeClause(cls[i]); 
+    for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
 
-    ClauseId id = ClauseIdUndef; 
+    ClauseId id = ClauseIdUndef;
     // Produce clauses in cross product:
     vec<Lit>& resolvent = add_tmp;
     for (int i = 0; i < pos.size(); i++)
@@ -569,7 +574,7 @@ bool SimpSolver::eliminateVar(Var v)
 
     // Free occurs list for this variable:
     occurs[v].clear(true);
-    
+
     // Free watchers lists for this variable, if possible:
     if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
     if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
@@ -589,7 +594,7 @@ bool SimpSolver::substitute(Var v, Lit x)
     eliminated[v] = true;
     setDecisionVar(v, false);
     const vec<CRef>& cls = occurs.lookup(v);
-    
+
     vec<Lit>& subst_clause = add_tmp;
     for (int i = 0; i < cls.size(); i++){
         Clause& c = ca[cls[i]];
@@ -641,9 +646,12 @@ bool SimpSolver::eliminate(bool turn_off_elim)
 
         gatherTouchedClauses();
         // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
-        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && 
-            !backwardSubsumptionCheck(true)){
-            ok = false; goto cleanup; }
+        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
+            && !backwardSubsumptionCheck(true))
+        {
+          ok = false;
+          goto cleanup;
+        }
 
         // Empty elim_heap and return immediately on user-interrupt:
         if (asynch_interrupt){
@@ -656,7 +664,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
         // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
         for (int cnt = 0; !elim_heap.empty(); cnt++){
             Var elim = elim_heap.removeMin();
-            
+
             if (asynch_interrupt) break;
 
             if (isEliminated(elim) || value(elim) != l_Undef) continue;
@@ -706,8 +714,10 @@ bool SimpSolver::eliminate(bool turn_off_elim)
     }
 
     if (verbosity >= 1 && elimclauses.size() > 0)
-        printf("|  Eliminated clauses:     %10.2f Mb                                      |\n", 
-               double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+      printf(
+          "|  Eliminated clauses:     %10.2f Mb                                "
+          "      |\n",
+          double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
 
     return ok;
 }
@@ -744,11 +754,11 @@ void SimpSolver::relocAll(ClauseAllocator& to)
     //
     for (int i = 0; i < subsumption_queue.size(); i++)
         ca.reloc(subsumption_queue[i], to);
-        // TODO reloc now takes the proof form the core solver 
+    // TODO reloc now takes the proof form the core solver
     // Temporary clause:
     //
     ca.reloc(bwdsub_tmpunit, to);
-    // TODO reloc now takes the proof form the core solver 
+    // TODO reloc now takes the proof form the core solver
 }
 
 
@@ -756,15 +766,17 @@ void SimpSolver::garbageCollect()
 {
     // Initialize the next region to a size corresponding to the estimated utilization degree. This
     // is not precise but should avoid some unnecessary reallocations for the new region:
-    ClauseAllocator to(ca.size() - ca.wasted()); 
+    ClauseAllocator to(ca.size() - ca.wasted());
 
     cleanUpClauses();
     to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
     relocAll(to);
     Solver::relocAll(to);
     if (verbosity >= 2)
-        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
-               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+      printf(
+          "|  Garbage collection:   %12d bytes => %12d bytes             |\n",
+          ca.size() * ClauseAllocator::Unit_Size,
+          to.size() * ClauseAllocator::Unit_Size);
     to.moveTo(ca);
-    // TODO: proof.finalizeUpdateId(); 
+    // TODO: proof.finalizeUpdateId();
 }