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).

21 files changed, 541 insertions, 724 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index c1aac33be..0b531c498 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -18,7 +18,6 @@
 
 #include "prop/bvminisat/simp/SimpSolver.h"
 #include "proof/clause_id.h"
-#include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -66,7 +65,6 @@ ClauseId BVMinisatSatSolver::addClause(SatClause& clause,
   // }
   ClauseId clause_id = ClauseIdError;
   d_minisat->addClause(minisat_clause, clause_id);
-  THEORY_PROOF(Assert(clause_id != ClauseIdError););
   return clause_id;
 }
 
@@ -76,14 +74,14 @@ SatValue BVMinisatSatSolver::propagate() {
 
 void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) {
   d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit)));
-  markUnremovable(lit); 
+  markUnremovable(lit);
 }
 
 void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) {
   std::vector<BVMinisat::Lit> minisat_explanation;
   d_minisat->explain(toMinisatLit(lit), minisat_explanation);
   for (unsigned i = 0; i < minisat_explanation.size(); ++i) {
-    explanation.push_back(toSatLiteral(minisat_explanation[i])); 
+    explanation.push_back(toSatLiteral(minisat_explanation[i]));
   }
 }
 
@@ -104,12 +102,6 @@ void BVMinisatSatSolver::popAssumption() {
   d_minisat->popAssumption();
 }
 
-void BVMinisatSatSolver::setResolutionProofLog(
-    proof::ResolutionBitVectorProof* bvp)
-{
-  d_minisat->setProofLog( bvp );
-}
-
 SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
   return d_minisat->newVar(true, true, !canErase);
 }
@@ -148,9 +140,7 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
   return result;
 }
 
-bool BVMinisatSatSolver::ok() const {
-  return d_minisat->okay(); 
-}
+bool BVMinisatSatSolver::ok() const { return d_minisat->okay(); }
 
 void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
   // TODO add assertion to check the call was after an unsat call
@@ -160,11 +150,11 @@ void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
 }
 
 SatValue BVMinisatSatSolver::value(SatLiteral l){
-	return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
+  return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
 }
 
 SatValue BVMinisatSatSolver::modelValue(SatLiteral l){
-	return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
+  return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
 }
 
 void BVMinisatSatSolver::unregisterVar(SatLiteral lit) {
@@ -309,17 +299,3 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
 
 } /* namespace CVC4::prop */
 } /* namespace CVC4 */
-
-namespace CVC4 {
-template<>
-prop::SatLiteral toSatLiteral< BVMinisat::Solver>(BVMinisat::Solver::TLit lit) {
-  return prop::BVMinisatSatSolver::toSatLiteral(lit);
-} 
-
-template<>
-void toSatClause< BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl,
-                                        prop::SatClause& sat_cl) {
-  prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl);
-}
-
-}
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 01a0a518e..f93dc8048 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -21,8 +21,6 @@
 #include <memory>
 
 #include "context/cdo.h"
-#include "proof/clause_id.h"
-#include "proof/resolution_bitvector_proof.h"
 #include "prop/bv_sat_solver_notify.h"
 #include "prop/bvminisat/simp/SimpSolver.h"
 #include "prop/sat_solver.h"
@@ -57,8 +55,8 @@ class BVMinisatSatSolver : public BVSatSolverInterface,
     }
   };
 
-	std::unique_ptr<BVMinisat::SimpSolver> d_minisat;
-	std::unique_ptr<MinisatNotify> d_minisatNotify;
+  std::unique_ptr<BVMinisat::SimpSolver> d_minisat;
+  std::unique_ptr<MinisatNotify> d_minisatNotify;
 
   unsigned d_assertionsCount;
   context::CDO<unsigned> d_assertionsRealCount;
@@ -79,6 +77,7 @@ public:
   ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
   {
     Unreachable() << "Minisat does not support native XOR reasoning";
+    return ClauseIdError;
   }
 
   SatValue propagate() override;
@@ -123,8 +122,6 @@ public:
 
   void popAssumption() override;
 
-  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) override;
-
  private:
   /* Disable the default constructor. */
   BVMinisatSatSolver() = delete;
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 84ab62fd8..f7ba14acd 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -29,11 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/output.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
-#include "proof/clause_id.h"
-#include "proof/proof_manager.h"
-#include "proof/resolution_bitvector_proof.h"
-#include "proof/sat_proof.h"
-#include "proof/sat_proof_implementation.h"
 #include "prop/bvminisat/mtl/Sort.h"
 #include "theory/interrupted.h"
 #include "util/utility.h"
@@ -170,8 +165,7 @@ Solver::Solver(CVC4::context::Context* context)
       ,
       conflict_budget(-1),
       propagation_budget(-1),
-      asynch_interrupt(false),
-      d_bvp(NULL)
+      asynch_interrupt(false)
 {
   // Create the constant variables
   varTrue = newVar(true, false);
@@ -220,7 +214,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
     if (decisionLevel() > 0) {
       cancelUntil(0);
     }
-    
+
     if (!ok) {
       id = ClauseIdUndef;
       return false;
@@ -231,7 +225,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
     sort(ps);
     Lit p; int i, j;
     int falseLiteralsCount = 0;
-    
+
     for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
       // tautologies are ignored
       if (value(ps[i]) == l_True || ps[i] == ~p) {
@@ -245,82 +239,30 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
       }
 
       if (value(ps[i]) == l_False) {
-        if (!THEORY_PROOF_ON())
-          continue;
-        ++falseLiteralsCount;
+        continue;
       }
       ps[j++] = p = ps[i];
     }
-    
+
     ps.shrink(i - j);
 
     clause_added = true;
 
-    Assert(falseLiteralsCount == 0 || THEORY_PROOF_ON());
-
     if(falseLiteralsCount == 0) {
       if (ps.size() == 0) {
-        Assert(!THEORY_PROOF_ON());
         return ok = false;
       }
       else if (ps.size() == 1){
-        if(d_bvp){ id = d_bvp->getSatProof()->registerUnitClause(ps[0], INPUT);}
         uncheckedEnqueue(ps[0]);
         CRef confl_ref = propagate();
         ok = (confl_ref == CRef_Undef);
-        if(d_bvp){ if (!ok) d_bvp->getSatProof()->finalizeProof(confl_ref); }
         return ok;
       } else {
         CRef cr = ca.alloc(ps, false);
         clauses.push(cr);
         attachClause(cr);
-        if(d_bvp){ id = d_bvp->getSatProof()->registerClause(cr, INPUT);}
-      }
-      return ok; 
-    }
-    
-    if (falseLiteralsCount != 0 && THEORY_PROOF_ON()) {
-      // we are in a conflicting state
-      if (ps.size() == falseLiteralsCount && falseLiteralsCount == 1) {
-        if(d_bvp){ id = d_bvp->getSatProof()->storeUnitConflict(ps[0], INPUT); }
-        if(d_bvp){ d_bvp->getSatProof()->finalizeProof(CVC4::BVMinisat::CRef_Lazy); }
-        return ok = false;
-      }
-
-      assign_lt lt(*this);
-      sort(ps, lt);
-      
-      CRef cr = ca.alloc(ps, false);
-      clauses.push(cr);
-      attachClause(cr);
-      
-      if(d_bvp){id = d_bvp->getSatProof()->registerClause(cr, INPUT);}
-
-      if(ps.size() == falseLiteralsCount) {
-        if(d_bvp){ d_bvp->getSatProof()->finalizeProof(cr); }
-        return ok = false;
-      }
-      
-      // Check if it propagates
-      if (ps.size() == falseLiteralsCount + 1) {
-        Clause& cl = ca[cr];
-
-        Assert(value(cl[0]) == l_Undef);
-        uncheckedEnqueue(cl[0], cr);
-        Assert(cl.size() > 1);
-        CRef confl = propagate();
-        ok = (confl == CRef_Undef);
-        if(!ok) {
-          if(d_bvp){
-            if(ca[confl].size() == 1) {
-              id = d_bvp->getSatProof()->storeUnitConflict(ca[confl][0], LEARNT);
-              d_bvp->getSatProof()->finalizeProof(CVC4::BVMinisat::CRef_Lazy);
-            } else {
-              d_bvp->getSatProof()->finalizeProof(confl);
-            }
-          }
-        }
       }
+      return ok;
     }
     return ok;
 }
@@ -338,9 +280,6 @@ void Solver::attachClause(CRef cr) {
 
 void Solver::detachClause(CRef cr, bool strict) {
   const Clause& clause = ca[cr];
-  if (d_bvp)
-  {
-    d_bvp->getSatProof()->markDeleted(cr); }
 
   assert(clause.size() > 1);
 
@@ -425,23 +364,24 @@ Lit Solver::pickBranchLit()
     return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
 }
 
-
 /*_________________________________________________________________________________________________
 |
-|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
-|  
+|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->
+[void]
+|
 |  Description:
 |    Analyze conflict and produce a reason clause.
-|  
+|
 |    Pre-conditions:
 |      * 'out_learnt' is assumed to be cleared.
 |      * Current decision level must be greater than root level.
-|  
+|
 |    Post-conditions:
 |      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
-|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the 
-|        rest of literals. There may be others from the same level though.
-|  
+|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision
+level of the |        rest of literals. There may be others from the same level
+though.
+|
 |________________________________________________________________________________________________@*/
 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip)
 {
@@ -454,8 +394,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
     int index   = trail.size() - 1;
 
     bool done = false;
-    
-    if(d_bvp){ d_bvp->getSatProof()->startResChain(confl); }
 
     do{
         assert(confl != CRef_Undef); // (otherwise should be UIP)
@@ -477,13 +415,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
               out_learnt.push(q);
           }
 
-          if (level(var(q)) == 0)
-          {
-            if (d_bvp)
-            {
-              d_bvp->getSatProof()->resolveOutUnit(q);
-            }
-          }
         }
 
         // Select next clause to look at:
@@ -493,10 +424,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
         seen[var(p)] = 0;
         pathC--;
 
-        if ( pathC > 0 && confl != CRef_Undef ) {
-          if(d_bvp){ d_bvp->getSatProof()->addResolutionStep(p, confl, sign(p));}
-        }
-
         switch (uip) {
         case UIP_FIRST:
           done = pathC == 0;
@@ -536,13 +463,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
               // Literal is not redundant
               out_learnt[j++] = out_learnt[i1];
             }
-            else
-            {
-              if (d_bvp)
-              {
-                d_bvp->getSatProof()->storeLitRedundant(out_learnt[i1]);
-              }
-            }
           }
         }
     }else if (ccmin_mode == 1){
@@ -640,10 +560,10 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
     return true;
 }
 
-/** 
+/**
  * Specialized analyzeFinal procedure where we test the consistency
  * of the assumptions before backtracking bellow the assumption level.
- * 
+ *
  * @param p the original uip (may be unit)
  * @param confl_clause the conflict clause
  * @param out_conflict the conflict in terms of assumptions we are building
@@ -653,14 +573,14 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
   assert (decisionLevel() == assumptions.size());
   assert (level(var(p)) == assumptions.size());
 
-  out_conflict.clear(); 
-  
+  out_conflict.clear();
+
   Clause& cl = ca[confl_clause];
   for (int i = 0; i < cl.size(); ++i) {
     seen[var(cl[i])] = 1;
   }
 
-  int end = options::proof() ? 0 :  trail_lim[0];
+  int end = trail_lim[0];
   for (int i = trail.size() - 1; i >= end; i--) {
     Var x = var(trail[i]);
     if (seen[x]) {
@@ -670,44 +590,31 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
           if (marker[x] == 2) {
             assert (level(x) > 0);
             out_conflict.push(~trail[i]);
-          } else {
-            if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); }
           }
-        } else {
-          if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~p);} 
         }
       } else {
         Clause& clause = ca[reason(x)];
-        if(d_bvp){d_bvp->getSatProof()->addResolutionStep(trail[i],reason(x), sign(trail[i]));}
 
         for (int j = 1; j < clause.size(); j++)
         {
           if (level(var(clause[j])) > 0) seen[var(clause[j])] = 1;
-          if(d_bvp){
-            if (level(var(clause[j])) == 0)
-            {
-              d_bvp->getSatProof()->resolveOutUnit(clause[j]);
-              seen[var(clause[j])] =
-                  0;  // we don't need to resolve it out again
-            }
-          }
         }
       }
       seen[x] = 0;
     }
-    assert (seen[x] == 0); 
+    assert(seen[x] == 0);
   }
-  assert (out_conflict.size()); 
+  assert(out_conflict.size());
 }
 
 /*_________________________________________________________________________________________________
 |
 |  analyzeFinal : (p : Lit)  ->  [void]
-|  
+|
 |  Description:
-|    Specialized analysis procedure to express the final conflict in terms of assumptions.
-|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
-|    stores the result in 'out_conflict'.
+|    Specialized analysis procedure to express the final conflict in terms of
+assumptions. |    Calculates the (possibly empty) set of assumptions that led to
+the assignment of 'p', and |    stores the result in 'out_conflict'.
 |________________________________________________________________________________________________@*/
 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
 {
@@ -716,22 +623,14 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
       out_conflict.push(p);
     }
 
-    if(d_bvp){
-      if (level(var(p)) == 0 && d_bvp->isAssumptionConflict()) {
-        Assert(marker[var(p)] == 2);
-        if (reason(var(p)) == CRef_Undef) {
-          d_bvp->startBVConflict(p);
-        }
-      }
-    }
-    
-    if (decisionLevel() == 0 && !options::proof()) {
+    if (decisionLevel() == 0)
+    {
       return;
     }
 
     seen[var(p)] = 1;
-    int end = options::proof() ? 0 : trail_lim[0];
-    
+    int end = trail_lim[0];
+
     for (int i = trail.size()-1; i >= end; i--){
         Var x = var(trail[i]);
         if (seen[x]) {
@@ -744,26 +643,12 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
               }
             } else {
               Clause& clause = ca[reason(x)];
-              if(d_bvp){
-                    if (d_bvp->isAssumptionConflict() &&
-                        trail[i] == p) {
-                      d_bvp->startBVConflict(reason(x));
-                    } else {
-                      d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i]));
-                    }
-              }
               for (int j = 1; j < clause.size(); j++)
               {
                 if (level(var(clause[j])) > 0)
                 {
                   seen[var(clause[j])] = 1;
                 }
-                if(d_bvp){
-                  if (level(var(clause[j])) == 0)
-                  {
-                    d_bvp->getSatProof()->resolveOutUnit(clause[j]);
-                  }
-                }
               }
             }
             seen[x] = 0;
@@ -805,10 +690,9 @@ lbool Solver::propagateAssumptions() {
 lbool Solver::assertAssumption(Lit p, bool propagate) {
   // TODO need to somehow mark the assumption as unit in the current context?
   // it's not always unit though, but this would be useful for debugging
-  
+
   // assert(marker[var(p)] == 1);
 
- 
   if (decisionLevel() > assumptions.size()) {
     cancelUntil(assumptions.size());
   }
@@ -829,9 +713,9 @@ lbool Solver::assertAssumption(Lit p, bool propagate) {
   // run the propagation
   if (propagate) {
     only_bcp = true;
-    ccmin_mode = 0; 
+    ccmin_mode = 0;
     lbool result = search(-1);
-    return result; 
+    return result;
   } else {
     return l_True;
   }
@@ -841,18 +725,16 @@ void Solver::addMarkerLiteral(Var var) {
   // make sure it wasn't already marked
   Assert(marker[var] == 0);
   marker[var] = 1;
-  if(d_bvp){d_bvp->getSatProof()->registerAssumption(var);}
 }
 
-
 /*_________________________________________________________________________________________________
 |
 |  propagate : [void]  ->  [Clause*]
-|  
+|
 |  Description:
-|    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
-|    otherwise CRef_Undef.
-|  
+|    Propagates all enqueued facts. If a conflict arises, the conflicting clause
+is returned, |    otherwise CRef_Undef.
+|
 |    Post-conditions:
 |      * the propagation queue is empty, even if there was a conflict.
 |________________________________________________________________________________________________@*/
@@ -920,20 +802,24 @@ CRef Solver::propagate()
     return confl;
 }
 
-
 /*_________________________________________________________________________________________________
 |
 |  reduceDB : ()  ->  [void]
-|  
+|
 |  Description:
-|    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
-|    clauses are clauses that are reason to some assignment. Binary clauses are never removed.
+|    Remove half of the learnt clauses, minus the clauses locked by the current
+assignment. Locked |    clauses are clauses that are reason to some assignment.
+Binary clauses are never removed.
 |________________________________________________________________________________________________@*/
-struct reduceDB_lt { 
-    ClauseAllocator& ca;
-    reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
-    bool operator () (CRef x, CRef y) { 
-        return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } 
+struct reduceDB_lt
+{
+  ClauseAllocator& ca;
+  reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
+  bool operator()(CRef x, CRef y)
+  {
+    return ca[x].size() > 2
+           && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity());
+  }
 };
 void Solver::reduceDB()
 {
@@ -963,14 +849,6 @@ void Solver::removeSatisfied(vec<CRef>& cs)
       Clause& clause = ca[cs[i]];
       if (satisfied(clause))
       {
-        if (locked(clause))
-        {
-          // store a resolution of the literal clause propagated
-          if (d_bvp)
-          {
-            d_bvp->getSatProof()->storeUnitResolution(clause[0]);
-          }
-        }
         removeClause(cs[i]);
       }
         else
@@ -989,14 +867,14 @@ void Solver::rebuildOrderHeap()
     order_heap.build(vs);
 }
 
-
 /*_________________________________________________________________________________________________
 |
 |  simplify : [void]  ->  [bool]
-|  
+|
 |  Description:
-|    Simplify the clause database according to the current top-level assigment. Currently, the only
-|    thing done here is the removal of satisfied clauses, but more things can be put here.
+|    Simplify the clause database according to the current top-level assigment.
+Currently, the only |    thing done here is the removal of satisfied clauses,
+but more things can be put here.
 |________________________________________________________________________________________________@*/
 bool Solver::simplify()
 {
@@ -1021,19 +899,19 @@ bool Solver::simplify()
     return true;
 }
 
-
 /*_________________________________________________________________________________________________
 |
 |  search : (nof_conflicts : int) (params : const SearchParams&)  ->  [lbool]
-|  
+|
 |  Description:
-|    Search for a model the specified number of conflicts. 
+|    Search for a model the specified number of conflicts.
 |    NOTE! Use negative value for 'nof_conflicts' indicate infinity.
-|  
+|
 |  Output:
-|    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
-|    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
-|    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
+|    'l_True' if a partial assigment that is consistent with respect to the
+clauseset is found. If |    all variables are decision variables, this means
+that the clause set is satisfiable. 'l_False' |    if the clause set is
+unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
 |________________________________________________________________________________________________@*/
 lbool Solver::search(int nof_conflicts, UIP uip)
 {
@@ -1051,7 +929,6 @@ lbool Solver::search(int nof_conflicts, UIP uip)
 
             if (decisionLevel() == 0) {
               // can this happen for bv?
-              if(d_bvp){ d_bvp->getSatProof()->finalizeProof(confl);}
               return l_False;
             }
 
@@ -1067,59 +944,34 @@ lbool Solver::search(int nof_conflicts, UIP uip)
               learnts.push(cr);
               attachClause(cr);
               claBumpActivity(ca[cr]);
-              if(d_bvp){
-                 ClauseId id = d_bvp->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])));
-                 }
-                 if( d_bvp ){ d_bvp->getSatProof()->storeClauseGlue(id, cl_levels.size()); }
-                       )
-                 d_bvp->getSatProof()->endResChain(id);
-              }
             }
-            
+
             if (learnt_clause.size() == 1) {
               // learning a unit clause
-              if(d_bvp){ d_bvp->getSatProof()->endResChain(learnt_clause[0]);}
             }
-            
+
             //  if the uip was an assumption we are unsat
             if (level(var(p)) <= assumptions.size()) {
               for (int i = 0; i < learnt_clause.size(); ++i) {
-                assert (level(var(learnt_clause[i])) <= decisionLevel()); 
+                assert(level(var(learnt_clause[i])) <= decisionLevel());
                 seen[var(learnt_clause[i])] = 1;
               }
 
-              // Starting new resolution chain for bit-vector proof
-              if( d_bvp ){
-                if (cr == CRef_Undef) {
-                  d_bvp->startBVConflict(learnt_clause[0]);
-                }
-                else { 
-                  d_bvp->startBVConflict(cr);
-                }
-              }
               analyzeFinal(p, conflict);
-              if(d_bvp){ d_bvp->endBVConflict(conflict); }
               Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl;
               return l_False;
             }
 
             if (!CVC4::options::bvEagerExplanations()) {
-              // check if uip leads to a conflict 
+              // check if uip leads to a conflict
               if (backtrack_level < assumptions.size()) {
                 cancelUntil(assumptions.size());
                 uncheckedEnqueue(p, cr);
-              
+
                 CRef new_confl = propagate();
                 if (new_confl != CRef_Undef) {
                   // we have a conflict we now need to explain it
-                  // TODO: proof for analyzeFinal2
-                  if(d_bvp){ d_bvp->startBVConflict(new_confl); }
                   analyzeFinal2(p, new_confl, conflict);
-                  if(d_bvp){ d_bvp->endBVConflict(conflict); }
                   return l_False;
                 }
               }
@@ -1127,8 +979,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
 
             cancelUntil(backtrack_level);
             uncheckedEnqueue(p, cr);
-    
-         
+
             varDecayActivity();
             claDecayActivity();
 
@@ -1138,10 +989,17 @@ lbool Solver::search(int nof_conflicts, UIP uip)
                 max_learnts             *= learntsize_inc;
 
                 if (verbosity >= 1)
-                    printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", 
-                           (int)conflicts, 
-                           (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 
-                           (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
+                  printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
+                         (int)conflicts,
+                         (int)dec_vars
+                             - (trail_lim.size() == 0 ? trail.size()
+                                                      : trail_lim[0]),
+                         nClauses(),
+                         (int)clauses_literals,
+                         (int)max_learnts,
+                         nLearnts(),
+                         (double)learnts_literals / nLearnts(),
+                         progressEstimate() * 100);
             }
 
         }else{
@@ -1152,9 +1010,9 @@ lbool Solver::search(int nof_conflicts, UIP uip)
                   withinBudget(ResourceManager::Resource::BvSatConflictsStep);
             }
             catch (const CVC4::theory::Interrupted& e) {
-              // do some clean-up and rethrow 
-              cancelUntil(assumptions.size()); 
-              throw e; 
+              // do some clean-up and rethrow
+              cancelUntil(assumptions.size());
+              throw e;
             }
 
             if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0
@@ -1192,10 +1050,8 @@ lbool Solver::search(int nof_conflicts, UIP uip)
                     newDecisionLevel();
                 }else if (value(p) == l_False){
                     marker[var(p)] = 2;
-                    
-                    if(d_bvp){  d_bvp->markAssumptionConflict(); }
+
                     analyzeFinal(~p, conflict);
-                    if(d_bvp){ d_bvp->endBVConflict(conflict); }
                     Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl;
                     return l_False;
                 }else{
@@ -1283,7 +1139,7 @@ lbool Solver::solve_()
     conflict.clear();
 
     ccmin_mode = 0;
-    
+
     if (!ok) return l_False;
 
     solves++;
@@ -1324,31 +1180,20 @@ lbool Solver::solve_()
 
 //=================================================================================================
 // Bitvector propagations
-// 
+//
 
 void Solver::explain(Lit p, std::vector<Lit>& explanation) {
   Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl;
 
   // top level fact, no explanation necessary
   if (level(var(p)) == 0) {
-    if(d_bvp){
-          // the only way a marker variable is 
-       if (reason(var(p)) == CRef_Undef) {
-          d_bvp->startBVConflict(p);
-          vec<Lit> confl;
-          confl.push(p);
-          d_bvp->endBVConflict(confl);
-          return;
-       }
-    }
-    if (!THEORY_PROOF_ON())
-      return;
+    return;
   }
-  
+
   seen[var(p)] = 1;
 
   // if we are called at decisionLevel = 0 trail_lim is empty
-  int bottom = options::proof() ? 0 : trail_lim[0];
+  int bottom = trail_lim[0];
   for (int i = trail.size()-1; i >= bottom; i--){
     Var x = var(trail[i]);
     if (seen[x]) {
@@ -1358,21 +1203,12 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) {
           explanation.push_back(trail[i]);
         } else {
           Assert(level(x) == 0);
-          if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); }
          }
-        
       } else {
         Clause& clause = ca[reason(x)];
-        if(d_bvp){
-          if (p == trail[i]) {
-            d_bvp->startBVConflict(reason(var(p)));
-          } else {
-            d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i]));
-          }
-        }
         for (int j = 1; j < clause.size(); j++)
         {
-          if (level(var(clause[j])) > 0 || options::proof())
+          if (level(var(clause[j])) > 0)
           {
             seen[var(clause[j])] = 1;
           }
@@ -1382,28 +1218,11 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) {
     }
   }
   seen[var(p)] = 0;
-
-  if(d_bvp){
-    vec<Lit> conflict_clause;
-    conflict_clause.push(p);
-    for(unsigned i = 0; i < explanation.size(); ++i) {
-      conflict_clause.push(~explanation[i]);
-    }
-    d_bvp->endBVConflict(conflict_clause);
-  }
-}
-
-void Solver::setProofLog(proof::ResolutionBitVectorProof* bvp)
-{
-  d_bvp = bvp;
-  d_bvp->initSatProof(this);
-  d_bvp->getSatProof()->registerTrueLit(mkLit(varTrue, false));
-  d_bvp->getSatProof()->registerFalseLit(mkLit(varFalse, true));
 }
 
 //=================================================================================================
 // Writing CNF to DIMACS:
-// 
+//
 // FIXME: this needs to be rewritten completely.
 
 static Var mapVar(Var x, vec<Var>& map, Var& max)
@@ -1454,7 +1273,7 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
     for (int i = 0; i < clauses.size(); i++)
         if (!satisfied(ca[clauses[i]]))
             cnt++;
-        
+
     for (int i = 0; i < clauses.size(); i++)
         if (!satisfied(ca[clauses[i]])){
           Clause& clause = ca[clauses[i]];
@@ -1494,8 +1313,7 @@ void Solver::relocAll(ClauseAllocator& to)
             Lit p = mkLit(v, s);
             // 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, d_bvp ? d_bvp->getSatProof() : NULL);
+            for (int j = 0; j < ws.size(); j++) ca.reloc(ws[j].cref, to);
         }
 
     // All reasons:
@@ -1504,20 +1322,16 @@ void Solver::relocAll(ClauseAllocator& to)
         Var v = var(trail[i]);
 
         if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
-          ca.reloc(vardata[v].reason, to, d_bvp ? d_bvp->getSatProof() : NULL);
+          ca.reloc(vardata[v].reason, to);
     }
 
     // All learnt:
     //
-    for (int i = 0; i < learnts.size(); i++)
-      ca.reloc(learnts[i], to, d_bvp ? d_bvp->getSatProof() : NULL);
+    for (int i = 0; i < learnts.size(); i++) ca.reloc(learnts[i], to);
 
     // All original:
     //
-    for (int i = 0; i < clauses.size(); i++)
-      ca.reloc(clauses[i], to, d_bvp ? d_bvp->getSatProof() : NULL);
-
-    if(d_bvp){ d_bvp->getSatProof()->finishUpdateCRef(); }
+    for (int i = 0; i < clauses.size(); i++) ca.reloc(clauses[i], to);
 }
 
 
@@ -1525,33 +1339,28 @@ void Solver::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()); 
-    Debug("bvminisat") << " BVMinisat::Garbage collection \n"; 
+    ClauseAllocator to(ca.size() - ca.wasted());
+    Debug("bvminisat") << " BVMinisat::Garbage collection \n";
     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);
 }
 
-void ClauseAllocator::reloc(CRef& cr,
-                            ClauseAllocator& to,
-                            CVC4::TSatProof<Solver>* proof)
+void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to)
 {
-  CRef old = cr;  // save the old reference
-
   Clause& c = operator[](cr);
   if (c.reloced()) { cr = c.relocation(); return; }
-  
+
   cr = to.alloc(c, c.learnt());
   c.relocate(cr);
-  if (proof)
-  {
-    proof->updateCRef(old, cr);
-  }
-  
-  // Copy extra data-fields: 
-  // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
+
+  // Copy extra data-fields:
+  // (This could be cleaned-up. Generalize Clause-constructor to be applicable
+  // here instead?)
   to[cr].mark(c.mark());
   if (to[cr].learnt())         to[cr].activity() = c.activity();
   else if (to[cr].has_extra()) to[cr].calcAbstraction();
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 7fad72d6d..f2721c88d 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -25,7 +25,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "context/context.h"
 #include "proof/clause_id.h"
-#include "proof/sat_proof.h"
 #include "prop/bvminisat/core/SolverTypes.h"
 #include "prop/bvminisat/mtl/Alg.h"
 #include "prop/bvminisat/mtl/Heap.h"
@@ -39,11 +38,6 @@ namespace BVMinisat {
 class Solver;
 }
 
-// TODO (aozdemir) replace this forward declaration with an include
-namespace proof {
-class ResolutionBitVectorProof;
-}
-
 namespace BVMinisat {
 
 /** Interface for minisat callbacks */
@@ -71,11 +65,10 @@ public:
 //=================================================================================================
 // Solver -- the main class:
 class Solver {
-    friend class CVC4::TSatProof< CVC4::BVMinisat::Solver>;
 public:
     typedef Var TVar;
     typedef Lit TLit;
-    typedef Clause TClause; 
+    typedef Clause TClause;
     typedef CRef TCRef;
     typedef vec<Lit> TLitVec;
 
@@ -109,12 +102,17 @@ public:
     Var     trueVar() const { return varTrue; }
     Var     falseVar() const { return varFalse; }
 
-
-    bool    addClause (const vec<Lit>& ps, ClauseId& id);                     // Add a clause to the solver. 
+    bool addClause(const vec<Lit>& ps,
+                   ClauseId& id);  // Add a clause to the solver.
     bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.
-    bool    addClause (Lit p, ClauseId& id);                                  // Add a unit clause to the solver. 
-    bool    addClause (Lit p, Lit q, ClauseId& id);                           // Add a binary clause to the solver. 
-    bool    addClause (Lit p, Lit q, Lit r, ClauseId& id);                    // Add a ternary clause to the solver. 
+    bool addClause(Lit p, ClauseId& id);  // Add a unit clause to the solver.
+    bool addClause(Lit p,
+                   Lit q,
+                   ClauseId& id);  // Add a binary clause to the solver.
+    bool addClause(Lit p,
+                   Lit q,
+                   Lit r,
+                   ClauseId& id);  // Add a ternary clause to the solver.
     bool    addClause_(      vec<Lit>& ps, ClauseId& id);                     // Add a clause to the solver without making superflous internal copy. Will
                                                                 // change the passed vector 'ps'.
 
@@ -141,9 +139,9 @@ public:
     void    toDimacs     (const char* file, Lit p);
     void    toDimacs     (const char* file, Lit p, Lit q);
     void    toDimacs     (const char* file, Lit p, Lit q, Lit r);
-    
+
     // Variable mode:
-    // 
+    //
     void    setPolarity    (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
     void    setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
 
@@ -211,13 +209,12 @@ public:
 
     void addMarkerLiteral(Var var);
 
-    bool need_to_propagate;             // true if we added new clauses, set to true in propagation 
+    bool need_to_propagate;  // true if we added new clauses, set to true in
+                             // propagation
     bool only_bcp;                      // solving mode in which only boolean constraint propagation is done
     void setOnlyBCP (bool val) { only_bcp = val;}
     void explain(Lit l, std::vector<Lit>& explanation);
 
-    void setProofLog(CVC4::proof::ResolutionBitVectorProof* bvp);
-
    protected:
 
     // has a clause been added
@@ -293,9 +290,6 @@ public:
     int64_t             conflict_budget;    // -1 means no budget.
     int64_t             propagation_budget; // -1 means no budget.
     bool                asynch_interrupt;
-    
-    //proof log
-    CVC4::proof::ResolutionBitVectorProof* d_bvp;
 
     // Main internal methods:
     //
@@ -458,13 +452,15 @@ inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
 inline int      Solver::nVars         ()      const   { return vardata.size(); }
 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
-inline void     Solver::setDecisionVar(Var v, bool b) 
-{ 
-    if      ( b && !decision[v]) dec_vars++;
-    else if (!b &&  decision[v]) dec_vars--;
+inline void Solver::setDecisionVar(Var v, bool b)
+{
+  if (b && !decision[v])
+    dec_vars++;
+  else if (!b && decision[v])
+    dec_vars--;
 
-    decision[v] = b;
-    insertVarOrder(v);
+  decision[v] = b;
+  insertVarOrder(v);
 }
 inline void     Solver::setConfBudget(int64_t x){ conflict_budget    = conflicts    + x; }
 inline void     Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h
index 302db104f..cf9ce7e15 100644
--- a/src/prop/bvminisat/core/SolverTypes.h
+++ b/src/prop/bvminisat/core/SolverTypes.h
@@ -86,15 +86,14 @@ struct LitHashFunction {
 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.
 
 #ifndef l_True
 #define l_True  (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
@@ -121,10 +120,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,14 +164,14 @@ class Clause {
         header.reloced   = 0;
         header.size      = ps.size();
 
-        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.learnt)
-                data[header.size].act = 0; 
-            else 
-                calcAbstraction(); }
+              data[header.size].act = 0;
+            else
+              calcAbstraction();
+        }
     }
 
 public:
@@ -256,9 +257,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
     }
 
-    void reloc(CRef& cr,
-               ClauseAllocator& to,
-               CVC4::TSatProof<Solver>* proof = NULL);
+    void reloc(CRef& cr, ClauseAllocator& to);
 };
 
 
@@ -275,7 +274,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); }
     // Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }
     Vec&  operator[](const Idx& idx){ return occs[toInt(idx)]; }
@@ -334,13 +333,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
@@ -363,15 +361,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/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 6641310cc..9429e4ced 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -23,7 +23,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "proof/clause_id.h"
-#include "proof/proof.h"
 #include "prop/bvminisat/mtl/Sort.h"
 #include "prop/bvminisat/utils/System.h"
 
@@ -64,7 +63,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* context)
       asymm_lits(0),
       eliminated_vars(0),
       elimorder(1),
-      use_simplification(!PROOF_ON()),
+      use_simplification(true),
       occurs(ClauseDeleted(ca)),
       elim_heap(ElimLt(n_occ)),
       bwdsub_assigns(0),
@@ -94,7 +93,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* context)
 
 SimpSolver::~SimpSolver()
 {
-  //  CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time); 
+  //  CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time);
 }
 
 
@@ -111,7 +110,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) {
         touched   .push(0);
         elim_heap .insert(v);
         if (freeze) {
-          setFrozen(v, true); 
+          setFrozen(v, true);
         }
     }
     return v;
@@ -122,7 +121,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) {
 lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 {
     only_bcp = false;
-  
+
     vec<Var> extra_frozen;
     lbool    result = l_True;
 
@@ -210,14 +209,15 @@ void SimpSolver::removeClause(CRef cr)
   const Clause& clause = ca[cr];
 
   if (use_simplification)
+  {
     for (int i = 0; i < clause.size(); i++)
     {
       n_occ[toInt(clause[i])]--;
       updateElimHeap(var(clause[i]));
       occurs.smudge(var(clause[i]));
     }
-
-    Solver::removeClause(cr);
+  }
+  Solver::removeClause(cr);
 }
 
 
@@ -546,9 +546,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;
@@ -565,8 +566,7 @@ 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]);
 
     // Produce clauses in cross product:
     vec<Lit>& resolvent = add_tmp;
@@ -580,7 +580,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);
@@ -600,7 +600,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& clause = ca[cls[i]];
@@ -643,7 +643,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
 {
 
   //  CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time);
-  
+
     if (!simplify())
         return false;
     else if (!use_simplification)
@@ -655,9 +655,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){
@@ -670,7 +673,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;
@@ -720,8 +723,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;
 
@@ -772,15 +777,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);
 }
 
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index ca447cea8..7cc5b16cd 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -19,7 +19,6 @@
 #ifdef CVC4_USE_CADICAL
 
 #include "base/check.h"
-#include "proof/sat_proof.h"
 
 namespace CVC4 {
 namespace prop {
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index a6a4b6859..c46cd5136 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -83,22 +83,13 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
     }
   }
 
-  if (PROOF_ON() && d_cnfProof)
-  {
-    d_cnfProof->pushCurrentDefinition(node);
-  }
-
   ClauseId clause_id = d_satSolver->addClause(c, d_removable);
   if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added)
 
-  if (PROOF_ON() && d_cnfProof)
+  if (d_cnfProof && clause_id != ClauseIdError)
   {
-    if (clause_id != ClauseIdError)
-    {
-      d_cnfProof->registerConvertedClause(clause_id);
-    }
-    d_cnfProof->popCurrentDefinition();
-  };
+    d_cnfProof->registerConvertedClause(clause_id);
+  }
 }
 
 void CnfStream::assertClause(TNode node, SatLiteral a) {
@@ -171,11 +162,17 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
     // non-empty and that we are not associating a bogus assertion with the
     // clause. This should be ok because we use the mapping back to assertions
     // for clauses from input assertions only.
-    PROOF(if (d_cnfProof) { d_cnfProof->pushCurrentAssertion(Node::null()); });
+    if (d_cnfProof)
+    {
+      d_cnfProof->pushCurrentAssertion(Node::null());
+    }
 
     lit = toCNF(n, false);
 
-    PROOF(if (d_cnfProof) { d_cnfProof->popCurrentAssertion(); });
+    if (d_cnfProof)
+    {
+      d_cnfProof->popCurrentAssertion();
+    }
 
     // Store backward-mappings
     // These may already exist
@@ -547,7 +544,6 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
     // If the node is a conjunction, we handle each conjunct separately
     for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
         conjunct != node_end; ++conjunct ) {
-      PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(*conjunct, node););
       convertAndAssert(*conjunct, false);
     }
   } else {
@@ -581,7 +577,6 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
     // If the node is a conjunction, we handle each conjunct separately
     for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
         conjunct != node_end; ++conjunct ) {
-      PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence((*conjunct).negate(), node.negate()););
       convertAndAssert(*conjunct, true);
     }
   }
@@ -658,8 +653,6 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
     clause[1] = q;
     assertClause(node, clause);
   } else {// Construct the
-    PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[0], node.negate()););
-    PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[1].negate(), node.negate()););
     // !(p => q) is the same as (p && ~q)
     convertAndAssert(node[0], false);
     convertAndAssert(node[1], true);
@@ -693,32 +686,23 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
 void TseitinCnfStream::convertAndAssert(TNode node,
                                         bool removable,
                                         bool negated,
-                                        ProofRule proof_id,
-                                        TNode from) {
+                                        bool input)
+{
   Debug("cnf") << "convertAndAssert(" << node
                << ", removable = " << (removable ? "true" : "false")
                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
   d_removable = removable;
-  PROOF
-    (if (d_cnfProof) {
-      Node assertion = negated ? node.notNode() : (Node)node;
-      Node from_assertion = negated? from.notNode() : (Node) from;
-
-      if (proof_id != RULE_INVALID) {
-        d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
-        d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
-      }
-      else {
-        d_cnfProof->pushCurrentAssertion(assertion);
-        d_cnfProof->registerAssertion(assertion, proof_id);
-      }
-    });
 
+  if (d_cnfProof)
+  {
+    d_cnfProof->pushCurrentAssertion(negated ? node.notNode() : (Node)node,
+                                     input);
+  }
   convertAndAssert(node, negated);
-  PROOF
-    (if (d_cnfProof) {
-      d_cnfProof->popCurrentAssertion();
-    });
+  if (d_cnfProof)
+  {
+    d_cnfProof->popCurrentAssertion();
+  }
 }
 
 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 40243e5b9..aec4257f2 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -186,10 +186,13 @@ class CnfStream {
    * @param node node to convert and assert
    * @param removable whether the sat solver can choose to remove the clauses
    * @param negated whether we are asserting the node negated
+   * @param input whether it is an input assertion (rather than a lemma). This
+   * information is only relevant for unsat core tracking.
    */
-  virtual void convertAndAssert(TNode node, bool removable, bool negated,
-                                ProofRule proof_id,
-                                TNode from = TNode::null()) = 0;
+  virtual void convertAndAssert(TNode node,
+                                bool removable,
+                                bool negated,
+                                bool input = false) = 0;
 
   /**
    * Get the node that is represented by the given SatLiteral.
@@ -269,12 +272,13 @@ class TseitinCnfStream : public CnfStream {
    * @param node the formula to assert
    * @param removable is this something that can be erased
    * @param negated true if negated
+   * @param input whether it is an input assertion (rather than a lemma). This
+   * information is only relevant for unsat core tracking.
    */
   void convertAndAssert(TNode node,
                         bool removable,
                         bool negated,
-                        ProofRule rule,
-                        TNode from = TNode::null()) override;
+                        bool input = false) override;
 
  private:
   /**
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index cf23758f1..92817a70c 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -19,8 +19,6 @@
 #include "prop/cryptominisat.h"
 
 #include "base/check.h"
-#include "proof/clause_id.h"
-#include "proof/sat_proof.h"
 
 #include <cryptominisat5/cryptominisat.h>
 
@@ -87,8 +85,9 @@ void CryptoMinisatSolver::init()
 CryptoMinisatSolver::~CryptoMinisatSolver() {}
 
 ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
-				       bool rhs,
-				       bool removable) {
+                                           bool rhs,
+                                           bool removable)
+{
   Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n";
 
   if (!d_okay) {
@@ -97,7 +96,7 @@ ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
   }
 
   ++(d_statistics.d_xorClausesAdded);
-  
+
   // ensure all sat literals have positive polarity by pushing
   // the negation on the result
   std::vector<CMSatVar> xor_clause;
@@ -119,36 +118,19 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
   }
 
   ++(d_statistics.d_clausesAdded);
-  
+
   std::vector<CMSat::Lit> internal_clause;
   toInternalClause(clause, internal_clause);
   bool nowOkay = d_solver->add_clause(internal_clause);
 
   ClauseId freshId;
-  if (THEORY_PROOF_ON())
-  {
-    freshId = ClauseId(ProofManager::currentPM()->nextId());
-    // If this clause results in a conflict, then `nowOkay` may be false, but
-    // we still need to register this clause as used. Thus, we look at
-    // `d_okay` instead
-    if (d_bvp && d_okay)
-    {
-      d_bvp->registerUsedClause(freshId, clause);
-    }
-  }
-  else
-  {
-    freshId = ClauseIdError;
-  }
+  freshId = ClauseIdError;
 
   d_okay &= nowOkay;
   return freshId;
 }
 
-bool CryptoMinisatSolver::ok() const {
-  return d_okay; 
-}
-
+bool CryptoMinisatSolver::ok() const { return d_okay; }
 
 SatVariable  CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
   d_solver->new_var();
@@ -208,19 +190,11 @@ SatValue CryptoMinisatSolver::value(SatLiteral l){
   return toSatLiteralValue(value);
 }
 
-SatValue CryptoMinisatSolver::modelValue(SatLiteral l){
-  return value(l); 
-}
+SatValue CryptoMinisatSolver::modelValue(SatLiteral l) { return value(l); }
 
 unsigned CryptoMinisatSolver::getAssertionLevel() const {
   Unreachable() << "No interface to get assertion level in Cryptominisat";
-  return -1; 
-}
-
-void CryptoMinisatSolver::setClausalProofLog(proof::ClausalBitVectorProof* bvp)
-{
-  d_bvp = bvp;
-  d_solver->set_drat(&bvp->getDratOstream(), false);
+  return -1;
 }
 
 // Satistics for CryptoMinisatSolver
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index d60855654..6d3b351b0 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -21,7 +21,6 @@
 
 #ifdef CVC4_USE_CRYPTOMINISAT
 
-#include "proof/clausal_bitvector_proof.h"
 #include "prop/sat_solver.h"
 
 // Cryptominisat has name clashes with the other Minisat implementations since
@@ -68,7 +67,6 @@ class CryptoMinisatSolver : public SatSolver
   SatValue modelValue(SatLiteral l) override;
 
   unsigned getAssertionLevel() const override;
-  void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override;
 
  private:
   class Statistics
@@ -97,7 +95,6 @@ class CryptoMinisatSolver : public SatSolver
   void init();
 
   std::unique_ptr<CMSat::SATSolver> d_solver;
-  proof::ClausalBitVectorProof* d_bvp;
   unsigned d_numVariables;
   bool d_okay;
   SatVariable d_true;
diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp
index 0440fcd4e..544a37a3e 100644
--- a/src/prop/kissat.cpp
+++ b/src/prop/kissat.cpp
@@ -19,7 +19,6 @@
 #ifdef CVC4_USE_KISSAT
 
 #include "base/check.h"
-#include "proof/sat_proof.h"
 
 namespace CVC4 {
 namespace prop {
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();
 }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index f74e52509..e71e681e5 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -99,17 +99,17 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
-  PROOF (
-         ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
-         );
+  if (options::unsatCores())
+  {
+    ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
+  }
 }
 
 void PropEngine::finishInit()
 {
   NodeManager* nm = NodeManager::currentNM();
-  d_cnfStream->convertAndAssert(nm->mkConst(true), false, false, RULE_GIVEN);
-  d_cnfStream->convertAndAssert(
-      nm->mkConst(false).notNode(), false, false, RULE_GIVEN);
+  d_cnfStream->convertAndAssert(nm->mkConst(true), false, false);
+  d_cnfStream->convertAndAssert(nm->mkConst(false).notNode(), false, false);
 }
 
 PropEngine::~PropEngine() {
@@ -126,18 +126,15 @@ void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as non-removable
-  d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN);
+  d_cnfStream->convertAndAssert(node, false, false, true);
 }
 
-void PropEngine::assertLemma(TNode node, bool negated,
-                             bool removable,
-                             ProofRule rule,
-                             TNode from) {
-  //Assert(d_inCheckSat, "Sat solver should be in solve()!");
+void PropEngine::assertLemma(TNode node, bool negated, bool removable)
+{
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
   // Assert as (possibly) removable
-  d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
+  d_cnfStream->convertAndAssert(node, removable, negated);
 }
 
 void PropEngine::addAssertionsToDecisionEngine(
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 9a2daee49..1df862568 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -103,11 +103,7 @@ class PropEngine
    * @param removable whether this lemma can be quietly removed based
    * on an activity heuristic (or not)
    */
-  void assertLemma(TNode node,
-                   bool negated,
-                   bool removable,
-                   ProofRule rule,
-                   TNode from = TNode::null());
+  void assertLemma(TNode node, bool negated, bool removable);
 
   /**
    * Pass a list of assertions from an AssertionPipeline to the decision engine.
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index d4b08ab71..1526e91b9 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -33,11 +33,6 @@
 
 namespace CVC4 {
 
-namespace proof {
-class ClausalBitVectorProof;
-class ResolutionBitVectorProof;
-}  // namespace proof
-
 namespace prop {
 
 class TheoryProxy;
@@ -58,7 +53,7 @@ public:
 
   /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
   virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
-  
+
   /**
    * Create a new boolean variable in the solver.
    * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
@@ -84,6 +79,7 @@ public:
   virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
   {
     Unimplemented() << "Solving under assumptions not implemented";
+    return SAT_VALUE_UNKNOWN;
   };
 
   /** Interrupt the solver */
@@ -101,10 +97,6 @@ public:
   /** Check if the solver is in an inconsistent state */
   virtual bool ok() const = 0;
 
-  virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {}
-
-  virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {}
-
 };/* class SatSolver */
 
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 41da4546e..d0ba4ca71 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -76,22 +76,12 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
 
-  LemmaProofRecipe* proofRecipe = NULL;
-  PROOF(proofRecipe = new LemmaProofRecipe;);
+  Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
 
-  Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
-
-  PROOF({
-      ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
-      ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
-
-      Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: "
-                       << std::endl;
-      proofRecipe->dump("pf::sat");
-
-      delete proofRecipe;
-      proofRecipe = NULL;
-    });
+  if (options::unsatCores())
+  {
+    ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
+  }
 
   Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
   if (theoryExplanation.getKind() == kind::AND) {