Remove old unsat cores (#6581)

This commit removes the remaining old proof code and the code to produce unsat cores based on it.

35 files changed, 24 insertions, 2393 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 083bce687..5362baad8 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -137,14 +137,8 @@ libcvc5_add_sources(
   printer/tptp/tptp_printer.cpp
   printer/tptp/tptp_printer.h
   proof/clause_id.h
-  proof/cnf_proof.cpp
-  proof/cnf_proof.h
   proof/dot/dot_printer.cpp
   proof/dot/dot_printer.h
-  proof/proof_manager.cpp
-  proof/proof_manager.h
-  proof/sat_proof.h
-  proof/sat_proof_implementation.h
   proof/unsat_core.cpp
   proof/unsat_core.h
   prop/bv_sat_solver_notify.h
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index ddffe8c12..880bbe0fb 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -200,9 +200,6 @@ name   = "SMT Layer"
 [[option.mode.OFF]]
   name = "off"
   help = "Do not produce unsat cores."
-[[option.mode.OLD_PROOF]]
-  name = "old-proof"
-  help = "Produce unsat cores from old proof infrastructure."
 [[option.mode.SAT_PROOF]]
   name = "sat-proof"
   help = "Produce unsat cores from SAT and preprocessing proofs."
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index beb8d75af..2f3a49ac2 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -19,7 +19,6 @@
 #include "expr/node_manager.h"
 #include "options/smt_options.h"
 #include "expr/lazy_proof.h"
-#include "proof/proof_manager.h"
 #include "smt/preprocess_proof_generator.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
@@ -103,10 +102,6 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
   {
     d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
   }
-  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-  {
-    ProofManager::currentPM()->addDependence(n, d_nodes[i]);
-  }
   d_nodes[i] = n;
 }
 
@@ -204,10 +199,6 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
       d_pppg->notifyNewAssert(newConjr, lcp);
     }
   }
-  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-  {
-    ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
-  }
   d_nodes[i] = newConjr;
   Assert(theory::Rewriter::rewrite(newConjr) == newConjr);
 }
diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index 8c97aabc7..44dafefcb 100644
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -21,7 +21,6 @@
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "proof/proof_manager.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 2b25098af..dc47c9c8e 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -21,7 +21,6 @@
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "proof/proof_manager.h"
 #include "prop/prop_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_preprocessor.h"
@@ -61,12 +60,6 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
     {
       imap[assertions->size()] = newSkolems[j];
       assertions->pushBackTrusted(newAsserts[j]);
-      // new assertions have a dependence on the node (old pf architecture)
-      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-      {
-        ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
-                                                 assertion);
-      }
     }
   }
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index f2724932f..e0a57ae5b 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -115,7 +115,6 @@ ITESimp::Statistics::Statistics()
 
 bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
 {
-  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
   bool result = true;
   bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
   if (simpDidALotOfWork)
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index fe515ed59..f27ff836a 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -188,7 +188,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
   Assert(assertionsToPreprocess->getRealAssertionsEnd()
          == assertionsToPreprocess->size());
   Assert(!options::incrementalSolving());
-  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
 
   context::Context fakeContext;
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index d88e901d7..921442f0e 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -69,12 +69,6 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult NonClausalSimp::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
-         || isProofEnabled())
-      << "Unsat cores with non-clausal simp only supported with new proofs. "
-         "Cores mode is "
-      << options::unsatCoresMode() << "\n";
-
   d_preprocContext->spendResource(Resource::PreprocessStep);
 
   theory::booleans::CircuitPropagator* propagator =
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 90a4b8240..1eb21cd96 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -20,7 +20,6 @@
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "proof/proof_manager.h"
 #include "prop/prop_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
@@ -58,12 +57,6 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
     {
       imap[assertions->size()] = newSkolems[j];
       assertions->pushBackTrusted(newAsserts[j]);
-      // new assertions have a dependence on the node (old pf architecture)
-      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-      {
-        ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
-                                                 assertion);
-      }
     }
   }
 
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
deleted file mode 100644
index 867977a29..000000000
--- a/src/proof/cnf_proof.cpp
+++ /dev/null
@@ -1,117 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Liana Hadarean, Andres Noetzli, Haniel Barbosa
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "proof/cnf_proof.h"
-
-#include "proof/clause_id.h"
-#include "proof/proof_manager.h"
-#include "prop/cnf_stream.h"
-#include "prop/minisat/minisat.h"
-#include "prop/sat_solver_types.h"
-
-namespace cvc5 {
-
-CnfProof::CnfProof(prop::CnfStream* stream,
-                   context::Context* ctx,
-                   const std::string& name)
-  : d_cnfStream(stream)
-  , d_clauseToAssertion(ctx)
-  , d_currentAssertionStack()
-  , d_cnfDeps()
-  , d_name(name)
-{
-  // Setting the proof object for the CnfStream
-  d_cnfStream->setProof(this);
-}
-
-CnfProof::~CnfProof() {}
-
-Node CnfProof::getAssertionForClause(ClauseId clause) {
-  ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause);
-  Assert(it != d_clauseToAssertion.end() && !(*it).second.isNull());
-  return (*it).second;
-}
-
-void CnfProof::registerConvertedClause(ClauseId clause)
-{
-  Assert(clause != ClauseIdUndef && clause != ClauseIdError
-         && clause != ClauseIdEmpty);
-  Node current_assertion = getCurrentAssertion();
-
-  Debug("proof:cnf") << "CnfProof::registerConvertedClause " << clause
-                     << " assertion = " << current_assertion << std::endl;
-
-  setClauseAssertion(clause, current_assertion);
-}
-
-void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
-  Debug("proof:cnf") << "CnfProof::setClauseAssertion "
-                     << clause << " assertion " << expr << std::endl;
-  // We can add the same clause from different assertions.  In this
-  // case we keep the first assertion. For example asserting a /\ b
-  // and then b /\ c where b is an atom, would assert b twice (note
-  // that since b is top level, it is not cached by the CnfStream)
-  //
-  // Note: If the current assertion associated with the clause is null, we
-  // update it because it means that it was previously added the clause without
-  // associating it with an assertion.
-  const auto& it = d_clauseToAssertion.find(clause);
-  if (it != d_clauseToAssertion.end() && (*it).second != Node::null())
-  {
-    return;
-  }
-
-  d_clauseToAssertion.insert(clause, expr);
-}
-
-void CnfProof::pushCurrentAssertion(Node assertion, bool isInput)
-{
-  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " << assertion
-                     << std::endl;
-
-  d_currentAssertionStack.push_back(std::pair<Node, bool>(assertion, isInput));
-
-  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion "
-                     << "new stack size = " << d_currentAssertionStack.size()
-                     << std::endl;
-}
-
-void CnfProof::popCurrentAssertion() {
-  Assert(d_currentAssertionStack.size());
-
-  Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
-                     << d_currentAssertionStack.back().first << std::endl;
-
-  d_currentAssertionStack.pop_back();
-
-  Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
-                     << "new stack size = " << d_currentAssertionStack.size()
-                     << std::endl;
-}
-
-Node CnfProof::getCurrentAssertion() {
-  Assert(d_currentAssertionStack.size());
-  return d_currentAssertionStack.back().first;
-}
-
-bool CnfProof::getCurrentAssertionKind()
-{
-  return d_currentAssertionStack.back().second;
-}
-
-}  // namespace cvc5
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
deleted file mode 100644
index 8e8f2bc91..000000000
--- a/src/proof/cnf_proof.h
+++ /dev/null
@@ -1,97 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Liana Hadarean, Haniel Barbosa, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A manager for CnfProofs.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__CNF_PROOF_H
-#define CVC5__CNF_PROOF_H
-
-#include <unordered_map>
-#include <unordered_set>
-
-#include "context/cdhashmap.h"
-#include "proof/clause_id.h"
-#include "proof/proof_manager.h"
-
-namespace cvc5 {
-namespace prop {
-  class CnfStream;
-  }  // namespace prop
-
-class CnfProof;
-
-typedef std::unordered_map<Node, Node> NodeToNode;
-typedef std::unordered_set<ClauseId> ClauseIdSet;
-
-typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
-typedef std::pair<Node, Node> NodePair;
-typedef std::set<NodePair> NodePairSet;
-
-typedef std::unordered_set<Node> NodeSet;
-
-class CnfProof {
-protected:
- cvc5::prop::CnfStream* d_cnfStream;
-
- /** Map from ClauseId to the assertion that lead to adding this clause **/
- ClauseIdToNode d_clauseToAssertion;
-
- /** Top of stack is assertion currently being converted to CNF. Also saves
-  * whether it is input (rather than a lemma). **/
- std::vector<std::pair<Node, bool>> d_currentAssertionStack;
-
- /** Map from top-level fact to facts/assertion that it follows from **/
- NodeToNode d_cnfDeps;
-
- ClauseIdSet d_explanations;
-
- // The clause ID of the unit clause defining the true SAT literal.
- ClauseId d_trueUnitClause;
- // The clause ID of the unit clause defining the false SAT literal.
- ClauseId d_falseUnitClause;
-
- std::string d_name;
-public:
- CnfProof(cvc5::prop::CnfStream* cnfStream,
-          context::Context* ctx,
-          const std::string& name);
- ~CnfProof();
-
- /** Methods for logging what the CnfStream does **/
- // map the clause back to the current assertion where it came from
- void registerConvertedClause(ClauseId clause);
-
- /** Clause is one of the clauses defining top-level assertion node*/
- void setClauseAssertion(ClauseId clause, Node node);
-
- /** Current assertion being converted and whether it is an input (rather than
-  * a lemma) */
- void pushCurrentAssertion(Node assertion, bool isInput = false);
- void popCurrentAssertion();
- Node getCurrentAssertion();
- bool getCurrentAssertionKind();
-
- /**
-  * Checks whether the assertion stack is empty.
-  */
- bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); }
-
- // accessors for the leaf assertions that are being converted to CNF
- Node getAssertionForClause(ClauseId clause);
-};/* class CnfProof */
-
-}  // namespace cvc5
-
-#endif /* CVC5__CNF_PROOF_H */
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
deleted file mode 100644
index f46317953..000000000
--- a/src/proof/proof_manager.cpp
+++ /dev/null
@@ -1,220 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Liana Hadarean, Morgan Deters, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- */
-
-#include "proof/proof_manager.h"
-
-#include "base/check.h"
-#include "context/context.h"
-#include "expr/node_visitor.h"
-#include "options/bv_options.h"
-#include "options/smt_options.h"
-#include "proof/clause_id.h"
-#include "proof/cnf_proof.h"
-#include "proof/sat_proof_implementation.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/smt_statistics_registry.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/output_channel.h"
-#include "theory/term_registration_visitor.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/valuation.h"
-#include "util/hash.h"
-
-namespace cvc5 {
-
-ProofManager::ProofManager(context::Context* context)
-    : d_context(context),
-      d_satProof(nullptr),
-      d_cnfProof(nullptr),
-      d_inputCoreFormulas(context),
-      d_outputCoreFormulas(context),
-      d_nextId(0),
-      d_deps(context)
-{
-}
-
-ProofManager::~ProofManager() {}
-
-ProofManager* ProofManager::currentPM() {
-  return smt::currentProofManager();
-}
-
-CoreSatProof* ProofManager::getSatProof()
-{
-  Assert(currentPM()->d_satProof);
-  return currentPM()->d_satProof.get();
-}
-
-CnfProof* ProofManager::getCnfProof()
-{
-  Assert(currentPM()->d_cnfProof);
-  return currentPM()->d_cnfProof.get();
-}
-
-void ProofManager::initSatProof(Minisat::Solver* solver)
-{
-  // Destroy old instance before initializing new one to avoid issues with
-  // registering stats
-  d_satProof.reset();
-  d_satProof.reset(new CoreSatProof(solver, d_context, "satproof::"));
-}
-
-void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
-                                context::Context* ctx)
-{
-  Assert(d_satProof != nullptr);
-
-  d_cnfProof.reset(new CnfProof(cnfStream, ctx, ""));
-
-  // true and false have to be setup in a special way
-  Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
-  Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode();
-
-  d_cnfProof->pushCurrentAssertion(true_node);
-  d_cnfProof->registerConvertedClause(d_satProof->getTrueUnit());
-  d_cnfProof->popCurrentAssertion();
-
-  d_cnfProof->pushCurrentAssertion(false_node);
-  d_cnfProof->registerConvertedClause(d_satProof->getFalseUnit());
-  d_cnfProof->popCurrentAssertion();
-}
-
-void ProofManager::traceDeps(TNode n, CDNodeSet* coreAssertions)
-{
-  Debug("cores") << "trace deps " << n << std::endl;
-  if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) ||
-      (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
-    return;
-  }
-  if (d_inputCoreFormulas.find(n) != d_inputCoreFormulas.end())
-  {
-    // originating formula was in core set
-    Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
-    coreAssertions->insert(n);
-  } else {
-    Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
-    if(d_deps.find(n) == d_deps.end()) {
-      InternalError()
-          << "Cannot trace dependence information back to input assertion:\n`"
-          << n << "'";
-    }
-    Assert(d_deps.find(n) != d_deps.end());
-    std::vector<Node> deps = (*d_deps.find(n)).second;
-
-    for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
-      Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
-      if( !(*i).isNull() ){
-        traceDeps(*i, coreAssertions);
-      }
-    }
-  }
-}
-
-void ProofManager::traceUnsatCore() {
-  Assert(options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF);
-  d_satProof->refreshProof();
-  IdToSatClause used_lemmas;
-  IdToSatClause used_inputs;
-  d_satProof->collectClausesUsed(used_inputs,
-                                 used_lemmas);
-
-  // At this point, there should be no assertions without a clause id
-  Assert(d_cnfProof->isAssertionStackEmpty());
-
-  IdToSatClause::const_iterator it = used_inputs.begin();
-  for(; it != used_inputs.end(); ++it) {
-    Node node = d_cnfProof->getAssertionForClause(it->first);
-
-    Debug("cores") << "core input assertion " << node << "\n";
-    // trace dependences back to actual assertions
-    // (this adds them to the unsat core)
-    traceDeps(node, &d_outputCoreFormulas);
-  }
-}
-
-bool ProofManager::unsatCoreAvailable() const {
-  return d_satProof->derivedEmptyClause();
-}
-
-std::vector<Node> ProofManager::extractUnsatCore()
-{
-  std::vector<Node> result;
-  output_core_iterator it = begin_unsat_core();
-  output_core_iterator end = end_unsat_core();
-  while ( it != end ) {
-    result.push_back(*it);
-    ++it;
-  }
-  return result;
-}
-
-void ProofManager::constructSatProof()
-{
-  if (!d_satProof->proofConstructed())
-  {
-    d_satProof->constructProof();
-  }
-}
-
-void ProofManager::getLemmasInUnsatCore(std::vector<Node>& lemmas)
-{
-  Assert(options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-      << "Cannot compute unsat core when proofs are off";
-  Assert(unsatCoreAvailable())
-      << "Cannot get unsat core at this time. Mabye the input is SAT?";
-  constructSatProof();
-  IdToSatClause used_lemmas;
-  IdToSatClause used_inputs;
-  d_satProof->collectClausesUsed(used_inputs, used_lemmas);
-  Debug("pf::lemmasUnsatCore") << "Retrieving all lemmas in unsat core\n";
-  IdToSatClause::const_iterator it;
-  for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it)
-  {
-    Node lemma = d_cnfProof->getAssertionForClause(it->first);
-    Debug("pf::lemmasUnsatCore") << "Retrieved lemma " << lemma << "\n";
-    lemmas.push_back(lemma);
-  }
-}
-
-void ProofManager::addCoreAssertion(Node formula)
-{
-  Debug("cores") << "assert: " << formula << std::endl;
-  d_deps[formula];  // empty vector of deps
-  d_inputCoreFormulas.insert(formula);
-}
-
-void ProofManager::addDependence(TNode n, TNode dep) {
-  if(dep != n) {
-    Debug("cores") << "dep: " << n << " : " << dep << std::endl;
-    if( !dep.isNull() && d_deps.find(dep) == d_deps.end()) {
-      Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl;
-    }
-    std::vector<Node> deps = d_deps[n].get();
-    deps.push_back(dep);
-    d_deps[n].set(deps);
-  }
-}
-
-void ProofManager::addUnsatCore(Node formula)
-{
-  Assert(d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
-  d_outputCoreFormulas.insert(formula);
-}
-
-}  // namespace cvc5
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
deleted file mode 100644
index 8d1bbc70c..000000000
--- a/src/proof/proof_manager.h
+++ /dev/null
@@ -1,124 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Liana Hadarean, Haniel Barbosa, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A manager for Proofs.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__PROOF_MANAGER_H
-#define CVC5__PROOF_MANAGER_H
-
-#include <memory>
-#include <unordered_map>
-#include <unordered_set>
-
-#include "context/cdhashmap.h"
-#include "context/cdhashset.h"
-#include "expr/node.h"
-#include "proof/clause_id.h"
-
-namespace cvc5 {
-
-// forward declarations
-namespace Minisat {
-  class Solver;
-}/* Minisat namespace */
-
-namespace prop {
-  class CnfStream;
-  }  // namespace prop
-
-class SmtEngine;
-
-template <class Solver> class TSatProof;
-typedef TSatProof<cvc5::Minisat::Solver> CoreSatProof;
-
-class CnfProof;
-
-typedef TSatProof<cvc5::Minisat::Solver> CoreSatProof;
-
-namespace prop {
-  typedef uint64_t SatVariable;
-  class SatLiteral;
-  typedef std::vector<SatLiteral> SatClause;
-  }  // namespace prop
-
-typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
-typedef context::CDHashSet<Node> CDNodeSet;
-typedef context::CDHashMap<Node, std::vector<Node>> CDNodeToNodes;
-typedef std::unordered_set<ClauseId> IdHashSet;
-
-class ProofManager {
-  context::Context* d_context;
-
-  std::unique_ptr<CoreSatProof> d_satProof;
-  std::unique_ptr<CnfProof> d_cnfProof;
-
-  // information that will need to be shared across proofs
-  CDNodeSet d_inputCoreFormulas;
-  CDNodeSet d_outputCoreFormulas;
-
-  int d_nextId;
-
-  CDNodeToNodes d_deps;
-
-public:
- ProofManager(context::Context* context);
- ~ProofManager();
-
- static ProofManager* currentPM();
-
- // initialization
- void initSatProof(Minisat::Solver* solver);
- void initCnfProof(cvc5::prop::CnfStream* cnfStream, context::Context* ctx);
-
- // getting various proofs
- static CoreSatProof* getSatProof();
- static CnfProof* getCnfProof();
-
- /** Public unsat core methods **/
- void addCoreAssertion(Node formula);
-
- void addDependence(TNode n, TNode dep);
- void addUnsatCore(Node formula);
-
- // trace dependences back to unsat core
- void traceDeps(TNode n, CDNodeSet* coreAssertions);
- void traceUnsatCore();
-
- typedef CDNodeSet::const_iterator output_core_iterator;
-
- output_core_iterator begin_unsat_core() const
- {
-   return d_outputCoreFormulas.begin();
- }
- output_core_iterator end_unsat_core() const
- {
-   return d_outputCoreFormulas.end();
- }
- size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
- std::vector<Node> extractUnsatCore();
-
- bool unsatCoreAvailable() const;
- void getLemmasInUnsatCore(std::vector<Node>& lemmas);
-
- int nextId() { return d_nextId++; }
-
-private:
- void constructSatProof();
-
-};/* class ProofManager */
-
-}  // namespace cvc5
-
-#endif /* CVC5__PROOF_MANAGER_H */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
deleted file mode 100644
index b85d0bc08..000000000
--- a/src/proof/sat_proof.h
+++ /dev/null
@@ -1,368 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Liana Hadarean, Tim King, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Resolution proof.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SAT__PROOF_H
-#define CVC5__SAT__PROOF_H
-
-#include <iosfwd>
-#include <set>
-#include <sstream>
-#include <unordered_map>
-#include <vector>
-
-#include "context/cdhashmap.h"
-#include "context/cdmaybe.h"
-#include "expr/node.h"
-#include "proof/clause_id.h"
-#include "proof/proof_manager.h"
-#include "util/statistics_stats.h"
-
-// Forward declarations.
-namespace cvc5 {
-class CnfProof;
-}  // namespace cvc5
-
-namespace cvc5 {
-/**
- * Helper debugging functions
- */
-template <class Solver>
-void printDebug(typename Solver::TLit l);
-template <class Solver>
-void printDebug(typename Solver::TClause& c);
-
-enum ClauseKind {
-  INPUT,
-  THEORY_LEMMA,  // we need to distinguish because we must reprove deleted
-                 // theory lemmas
-  LEARNT
-}; /* enum ClauseKind */
-
-template <class Solver>
-struct ResStep {
-  typename Solver::TLit lit;
-  ClauseId id;
-  bool sign;
-  ResStep(typename Solver::TLit l, ClauseId i, bool s)
-      : lit(l), id(i), sign(s) {}
-}; /* struct ResStep */
-
-template <class Solver>
-class ResChain {
- public:
-  typedef std::vector<ResStep<Solver> > ResSteps;
-  typedef std::set<typename Solver::TLit> LitSet;
-
-  ResChain(ClauseId start);
-  ~ResChain();
-
-  void addStep(typename Solver::TLit, ClauseId, bool);
-  bool redundantRemoved() {
-    return (d_redundantLits == NULL || d_redundantLits->empty());
-  }
-  void addRedundantLit(typename Solver::TLit lit);
-
-  // accessor methods
-  ClauseId getStart() const { return d_start; }
-  const ResSteps& getSteps() const { return d_steps; }
-  LitSet* getRedundant() const { return d_redundantLits; }
-
- private:
-  ClauseId d_start;
-  ResSteps d_steps;
-  LitSet* d_redundantLits;
-}; /* class ResChain */
-
-template <class Solver>
-class TSatProof {
- protected:
-  typedef ResChain<Solver> ResolutionChain;
-
-  typedef std::set<typename Solver::TLit> LitSet;
-  typedef std::set<typename Solver::TVar> VarSet;
-  typedef std::unordered_map<ClauseId, typename Solver::TCRef> IdCRefMap;
-  typedef std::unordered_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
-  typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap;
-  typedef context::CDHashMap<int, ClauseId> UnitIdMap;
-  typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap;
-  typedef std::unordered_map<ClauseId, uint64_t> IdProofRuleMap;
-  typedef std::vector<ResolutionChain*> ResStack;
-  typedef std::set<ClauseId> IdSet;
-  typedef std::vector<typename Solver::TLit> LitVector;
-  typedef std::unordered_map<ClauseId, typename Solver::TClause&>
-      IdToMinisatClause;
-  typedef std::unordered_map<ClauseId, LitVector*> IdToConflicts;
-
- public:
-  TSatProof(Solver* solver, context::Context* context,
-            const std::string& name, bool checkRes = false);
-  ~TSatProof();
-
-  void startResChain(typename Solver::TLit start);
-  void startResChain(typename Solver::TCRef start);
-  void addResolutionStep(typename Solver::TLit lit,
-                         typename Solver::TCRef clause, bool sign);
-  /**
-   * Pops the current resolution of the stack and stores it
-   * in the resolution map. Also registers the 'clause' parameter
-   * @param clause the clause the resolution is proving
-   */
-  // void endResChain(typename Solver::TCRef clause);
-  void endResChain(typename Solver::TLit lit);
-  void endResChain(ClauseId id);
-
-  /**
-   * Pops the current resolution of the stack *without* storing it.
-   */
-  void cancelResChain();
-
-  /**
-   * Stores in the current derivation the redundant literals that were
-   * eliminated from the conflict clause during conflict clause minimization.
-   * @param lit the eliminated literal
-   */
-  void storeLitRedundant(typename Solver::TLit lit);
-
-  /// update the CRef Id maps when Minisat does memory reallocation x
-  void updateCRef(typename Solver::TCRef old_ref,
-                  typename Solver::TCRef new_ref);
-  void finishUpdateCRef();
-
-  /**
-   * Constructs the empty clause resolution from the final conflict
-   *
-   * @param conflict
-   */
-  void finalizeProof(typename Solver::TCRef conflict);
-
-  /// clause registration methods
-
-  ClauseId registerClause(const typename Solver::TCRef clause, ClauseKind kind);
-  ClauseId registerUnitClause(const typename Solver::TLit lit, ClauseKind kind);
-  void registerTrueLit(const typename Solver::TLit lit);
-  void registerFalseLit(const typename Solver::TLit lit);
-
-  ClauseId getTrueUnit() const;
-  ClauseId getFalseUnit() const;
-
-  void registerAssumption(const typename Solver::TVar var);
-  ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl);
-
-  ClauseId storeUnitConflict(typename Solver::TLit lit, ClauseKind kind);
-
-  /**
-   * Marks the deleted clauses as deleted. Note we may still use them in the
-   * final
-   * resolution.
-   * @param clause
-   */
-  void markDeleted(typename Solver::TCRef clause);
-  bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); }
-  /**
-   * Constructs the resolution of ~q and resolves it with the current
-   * resolution thus eliminating q from the current clause
-   * @param q the literal to be resolved out
-   */
-  void resolveOutUnit(typename Solver::TLit q);
-  /**
-   * Constructs the resolution of the literal lit. Called when a clause
-   * containing lit becomes satisfied and is removed.
-   * @param lit
-   */
-  void storeUnitResolution(typename Solver::TLit lit);
-
-  /**
-   * Constructs the SAT proof for the given clause,
-   * by collecting the needed clauses in the d_seen
-   * data-structures, also notifying the proofmanager.
-   */
-  void constructProof(ClauseId id);
-  void constructProof() { constructProof(d_emptyClauseId); }
-  void refreshProof(ClauseId id);
-  void refreshProof() { refreshProof(d_emptyClauseId); }
-  bool proofConstructed() const;
-  void collectClauses(ClauseId id);
-  bool derivedEmptyClause() const;
-  prop::SatClause* buildClause(ClauseId id);
-
-  void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas);
-
-  void storeClauseGlue(ClauseId clause, int glue);
-
-  bool isInputClause(ClauseId id) const;
-  bool isLemmaClause(ClauseId id) const;
-  bool isAssumptionConflict(ClauseId id) const;
-
-  bool hasResolutionChain(ClauseId id) const;
-
-  /** Returns the resolution chain associated with id. Assert fails if
-   * hasResolution(id) does not hold. */
-  const ResolutionChain& getResolutionChain(ClauseId id) const;
-
-  const ClauseId& getEmptyClauseId() const { return d_emptyClauseId; }
-  const IdSet& getSeenLearnt() const { return d_seenLearnt; }
-  const IdToConflicts& getAssumptionConflicts() const
-  {
-    return d_assumptionConflictsDebug;
-  }
-
- private:
-  bool isUnit(ClauseId id) const;
-  typename Solver::TLit getUnit(ClauseId id) const;
-
-  bool isUnit(typename Solver::TLit lit) const;
-  ClauseId getUnitId(typename Solver::TLit lit) const;
-
-  void createLitSet(ClauseId id, LitSet& set);
-
-  /**
-   * Registers a ClauseId with a resolution chain res.
-   * Takes ownership of the memory associated with res.
-   */
-  void registerResolution(ClauseId id, ResolutionChain* res);
-
-
-  bool hasClauseIdForCRef(typename Solver::TCRef clause) const;
-  ClauseId getClauseIdForCRef(typename Solver::TCRef clause) const;
-
-  bool hasClauseIdForLiteral(typename Solver::TLit lit) const;
-  ClauseId getClauseIdForLiteral(typename Solver::TLit lit) const;
-
-  bool hasClauseRef(ClauseId id) const;
-  typename Solver::TCRef getClauseRef(ClauseId id) const;
-
-
-  const typename Solver::TClause& getClause(typename Solver::TCRef ref) const;
-
-  void getLitVec(ClauseId id, LitVector& vec);
-
-  bool checkResolution(ClauseId id);
-
-  /**
-   * Constructs a resolution tree that proves lit
-   * and returns the ClauseId for the unit clause lit
-   * @param lit the literal we are proving
-   *
-   * @return
-   */
-  ClauseId resolveUnit(typename Solver::TLit lit);
-
-  /**
-   * Does a depth first search on removed literals and adds the literals
-   * to be removed in the proper order to the stack.
-   *
-   * @param lit the literal we are recursing on
-   * @param removedSet the previously computed set of redundant literals
-   * @param removeStack the stack of literals in reverse order of resolution
-   */
-  void removedDfs(typename Solver::TLit lit, LitSet* removedSet,
-                  LitVector& removeStack, LitSet& inClause, LitSet& seen);
-  void removeRedundantFromRes(ResChain<Solver>* res, ClauseId id);
-
-  void print(ClauseId id) const;
-  void printRes(ClauseId id) const;
-  void printRes(const ResolutionChain& res) const;
-
-  std::unordered_map<ClauseId, int> d_glueMap;
-  struct Statistics {
-    IntStat d_numLearnedClauses;
-    IntStat d_numLearnedInProof;
-    IntStat d_numLemmasInProof;
-    AverageStat d_avgChainLength;
-    HistogramStat<uint64_t> d_resChainLengths;
-    HistogramStat<uint64_t> d_usedResChainLengths;
-    HistogramStat<uint64_t> d_clauseGlue;
-    HistogramStat<uint64_t> d_usedClauseGlue;
-    Statistics(const std::string& name);
-  };
-
-  const ClauseId d_emptyClauseId;
-  IdSet d_seenLearnt;
-  IdToConflicts d_assumptionConflictsDebug;
-
-  // Internal data.
-  Solver* d_solver;
-  context::Context* d_context;
-
-  // clauses
-  IdCRefMap d_idClause;
-  ClauseIdMap d_clauseId;
-  IdUnitMap d_idUnit;
-  UnitIdMap d_unitId;
-  IdHashSet d_deleted;
-  IdToSatClause d_deletedTheoryLemmas;
-
-  IdHashSet d_inputClauses;
-  IdHashSet d_lemmaClauses;
-  VarSet d_assumptions;             // assumption literals for bv solver
-  IdHashSet d_assumptionConflicts;  // assumption conflicts not actually added
-                                    // to SAT solver
-
-  // Resolutions.
-
-  /**
-   * Map from ClauseId to resolution chain corresponding proving the
-   * clause corresponding to the ClauseId. d_resolutionChains owns the
-   * memory of the ResChain* it contains.
-   */
-  IdResMap d_resolutionChains;
-
-   /*
-   * Stack containting current ResChain* we are working on. d_resStack
-   * owns the memory for the ResChain* it contains. Invariant: no
-   * ResChain* pointer can be both in d_resStack and
-   * d_resolutionChains. Memory ownership is transfered from
-   * d_resStack to d_resolutionChains via registerResolution.
-   */
-  ResStack d_resStack;
-  bool d_checkRes;
-
-  const ClauseId d_nullId;
-
-  // temporary map for updating CRefs
-  ClauseIdMap d_temp_clauseId;
-  IdCRefMap d_temp_idClause;
-
-  // unit conflict
-  context::CDMaybe<ClauseId> d_unitConflictId;
-
-  ClauseId d_trueLit;
-  ClauseId d_falseLit;
-
-  IdToSatClause d_seenInputs;
-  IdToSatClause d_seenLemmas;
-
-  bool d_satProofConstructed;
-  Statistics d_statistics;
-}; /* class TSatProof */
-
-template <class Solver>
-prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
-
-/**
- * Convert from minisat clause to SatClause
- *
- * @param minisat_cl
- * @param sat_cl
- */
-template <class Solver>
-void toSatClause(const typename Solver::TClause& minisat_cl,
-                 prop::SatClause& sat_cl);
-
-}  // namespace cvc5
-
-#endif /* CVC5__SAT__PROOF_H */
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
deleted file mode 100644
index c411ae741..000000000
--- a/src/proof/sat_proof_implementation.h
+++ /dev/null
@@ -1,1047 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Liana Hadarean, Tim King, Guy Katz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Resolution proof.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SAT__PROOF_IMPLEMENTATION_H
-#define CVC5__SAT__PROOF_IMPLEMENTATION_H
-
-#include "proof/clause_id.h"
-#include "proof/sat_proof.h"
-#include "prop/minisat/core/Solver.h"
-#include "prop/minisat/minisat.h"
-#include "prop/sat_solver_types.h"
-#include "smt/smt_statistics_registry.h"
-
-namespace cvc5 {
-
-template <class Solver>
-void printLit(typename Solver::TLit l) {
-  Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1;
-}
-
-template <class Solver>
-void printClause(const typename Solver::TClause& c) {
-  for (int i = 0; i < c.size(); i++) {
-    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
-  }
-}
-
-template <class Solver>
-void printClause(const std::vector<typename Solver::TLit>& c) {
-  for (unsigned i = 0; i < c.size(); i++) {
-    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
-  }
-}
-
-template <class Solver>
-void printLitSet(const std::set<typename Solver::TLit>& s) {
-  typename std::set<typename Solver::TLit>::const_iterator it = s.begin();
-  for (; it != s.end(); ++it) {
-    printLit<Solver>(*it);
-    Debug("proof:sat") << " ";
-  }
-  Debug("proof:sat") << std::endl;
-}
-
-// purely debugging functions
-template <class Solver>
-void printDebug(typename Solver::TLit l) {
-  Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl;
-}
-template <class Solver>
-void printDebug(typename Solver::TClause& c) {
-  for (int i = 0; i < c.size(); i++) {
-    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
-  }
-  Debug("proof:sat") << std::endl;
-}
-
-/**
- * Converts the clause associated to id to a set of literals
- *
- * @param id the clause id
- * @param set the clause converted to a set of literals
- */
-template <class Solver>
-void TSatProof<Solver>::createLitSet(ClauseId id, LitSet& set) {
-  Assert(set.empty());
-  if (isUnit(id)) {
-    set.insert(getUnit(id));
-    return;
-  }
-  if (id == d_emptyClauseId) {
-    return;
-  }
-  // if it's an assumption
-  if (d_assumptionConflictsDebug.find(id) != d_assumptionConflictsDebug.end()) {
-    LitVector* clause = d_assumptionConflictsDebug[id];
-    for (unsigned i = 0; i < clause->size(); ++i) {
-      set.insert(clause->operator[](i));
-    }
-    return;
-  }
-
-  typename Solver::TCRef ref = getClauseRef(id);
-  const typename Solver::TClause& c = getClause(ref);
-  for (int i = 0; i < c.size(); i++) {
-    set.insert(c[i]);
-  }
-}
-
-/**
- * Resolves clause1 and clause2 on variable var and stores the
- * result in clause1
- * @param v
- * @param clause1
- * @param clause2
- */
-template <class Solver>
-bool resolve(const typename Solver::TLit v,
-             std::set<typename Solver::TLit>& clause1,
-             std::set<typename Solver::TLit>& clause2, bool s) {
-  Assert(!clause1.empty());
-  Assert(!clause2.empty());
-  typename Solver::TLit var = sign(v) ? ~v : v;
-  if (s) {
-    // literal appears positive in the first clause
-    if (!clause2.count(~var)) {
-      if (Debug.isOn("proof:sat")) {
-        Debug("proof:sat") << "proof:resolve: Missing literal ";
-        printLit<Solver>(var);
-        Debug("proof:sat") << std::endl;
-      }
-      return false;
-    }
-    clause1.erase(var);
-    clause2.erase(~var);
-    typename std::set<typename Solver::TLit>::iterator it = clause2.begin();
-    for (; it != clause2.end(); ++it) {
-      clause1.insert(*it);
-    }
-  } else {
-    // literal appears negative in the first clause
-    if (!clause1.count(~var) || !clause2.count(var)) {
-      if (Debug.isOn("proof:sat")) {
-        Debug("proof:sat") << "proof:resolve: Missing literal ";
-        printLit<Solver>(var);
-        Debug("proof:sat") << std::endl;
-      }
-      return false;
-    }
-    clause1.erase(~var);
-    clause2.erase(var);
-    typename std::set<typename Solver::TLit>::iterator it = clause2.begin();
-    for (; it != clause2.end(); ++it) {
-      clause1.insert(*it);
-    }
-  }
-  return true;
-}
-
-/// ResChain
-template <class Solver>
-ResChain<Solver>::ResChain(ClauseId start)
-    : d_start(start), d_steps(), d_redundantLits(NULL) {}
-
-template <class Solver>
-ResChain<Solver>::~ResChain() {
-  if (d_redundantLits != NULL) {
-    delete d_redundantLits;
-  }
-}
-
-template <class Solver>
-void ResChain<Solver>::addStep(typename Solver::TLit lit, ClauseId id,
-                               bool sign) {
-  ResStep<Solver> step(lit, id, sign);
-  d_steps.push_back(step);
-}
-
-template <class Solver>
-void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) {
-  if (d_redundantLits) {
-    d_redundantLits->insert(lit);
-  } else {
-    d_redundantLits = new LitSet();
-    d_redundantLits->insert(lit);
-  }
-}
-
-/// SatProof
-template <class Solver>
-TSatProof<Solver>::TSatProof(Solver* solver,
-                             context::Context* context,
-                             const std::string& name,
-                             bool checkRes)
-    : d_emptyClauseId(ClauseIdEmpty),
-      d_seenLearnt(),
-      d_assumptionConflictsDebug(),
-      d_solver(solver),
-      d_context(context),
-      d_idClause(),
-      d_clauseId(),
-      d_idUnit(context),
-      d_unitId(context),
-      d_deleted(),
-      d_inputClauses(),
-      d_lemmaClauses(),
-      d_assumptions(),
-      d_assumptionConflicts(),
-      d_resolutionChains(d_context),
-      d_resStack(),
-      d_checkRes(checkRes),
-      d_nullId(-2),
-      d_temp_clauseId(),
-      d_temp_idClause(),
-      d_unitConflictId(context),
-      d_trueLit(ClauseIdUndef),
-      d_falseLit(ClauseIdUndef),
-      d_seenInputs(),
-      d_seenLemmas(),
-      d_satProofConstructed(false),
-      d_statistics(name)
-{
-}
-
-template <class Solver>
-TSatProof<Solver>::~TSatProof() {
-  // FIXME: double free if deleted clause also appears in d_seenLemmas?
-  IdToSatClause::const_iterator it = d_deletedTheoryLemmas.begin();
-  IdToSatClause::const_iterator end = d_deletedTheoryLemmas.end();
-
-  for (; it != end; ++it) {
-    ClauseId id = it->first;
-    // otherwise deleted in next loop
-    if (d_seenLemmas.find(id) == d_seenLemmas.end()) {
-      delete it->second;
-    }
-  }
-
-  IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin();
-  IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end();
-
-  for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) {
-    delete seen_lemma_it->second;
-  }
-
-  IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin();
-  IdToSatClause::const_iterator seen_input_end = d_seenInputs.end();
-
-  for (; seen_input_it != seen_input_end; ++seen_input_it) {
-    delete seen_input_it->second;
-  }
-
-  typedef typename IdResMap::const_iterator ResolutionChainIterator;
-  ResolutionChainIterator resolution_it = d_resolutionChains.begin();
-  ResolutionChainIterator resolution_it_end = d_resolutionChains.end();
-  for (; resolution_it != resolution_it_end; ++resolution_it) {
-    ResChain<Solver>* current = (*resolution_it).second;
-    delete current;
-  }
-
-  // It could be the case that d_resStack is not empty at destruction time
-  // (for example in the SAT case).
-  typename ResStack::const_iterator resolution_stack_it = d_resStack.begin();
-  typename ResStack::const_iterator resolution_stack_it_end = d_resStack.end();
-  for (; resolution_stack_it != resolution_stack_it_end;
-       ++resolution_stack_it) {
-    ResChain<Solver>* current = *resolution_stack_it;
-    delete current;
-  }
-}
-
-/**
- * Returns true if the resolution chain corresponding to id
- * does resolve to the clause associated to id
- * @param id
- *
- * @return
- */
-template <class Solver>
-bool TSatProof<Solver>::checkResolution(ClauseId id) {
-  if (d_checkRes) {
-    bool validRes = true;
-    Assert(hasResolutionChain(id));
-    const ResolutionChain& res = getResolutionChain(id);
-    LitSet clause1;
-    createLitSet(res.getStart(), clause1);
-    const typename ResolutionChain::ResSteps& steps = res.getSteps();
-    for (unsigned i = 0; i < steps.size(); i++) {
-      typename Solver::TLit var = steps[i].lit;
-      LitSet clause2;
-      createLitSet(steps[i].id, clause2);
-      if (!resolve<Solver>(var, clause1, clause2, steps[i].sign))
-      {
-        validRes = false;
-        break;
-      }
-    }
-    // compare clause we claimed to prove with the resolution result
-    if (isUnit(id)) {
-      // special case if it was a unit clause
-      typename Solver::TLit unit = getUnit(id);
-      validRes = clause1.size() == clause1.count(unit) && !clause1.empty();
-      return validRes;
-    }
-    if (id == d_emptyClauseId) {
-      return clause1.empty();
-    }
-
-    LitVector c;
-    getLitVec(id, c);
-
-    for (unsigned i = 0; i < c.size(); ++i) {
-      int count = clause1.erase(c[i]);
-      if (count == 0) {
-        if (Debug.isOn("proof:sat")) {
-          Debug("proof:sat")
-              << "proof:checkResolution::literal not in computed result ";
-          printLit<Solver>(c[i]);
-          Debug("proof:sat") << "\n";
-        }
-        validRes = false;
-      }
-    }
-    validRes = clause1.empty();
-    if (!validRes) {
-      if (Debug.isOn("proof:sat")) {
-        Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, "
-                              "unremoved literals: \n";
-        printLitSet<Solver>(clause1);
-        Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
-        printClause<Solver>(c);
-      }
-    }
-    return validRes;
-
-  } else {
-    return true;
-  }
-}
-
-/// helper methods
-template <class Solver>
-bool TSatProof<Solver>::hasClauseIdForCRef(typename Solver::TCRef ref) const {
-  return d_clauseId.find(ref) != d_clauseId.end();
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::getClauseIdForCRef(
-    typename Solver::TCRef ref) const {
-  if (d_clauseId.find(ref) == d_clauseId.end()) {
-    Debug("proof:sat") << "Missing clause \n";
-  }
-  Assert(hasClauseIdForCRef(ref));
-  return d_clauseId.find(ref)->second;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::hasClauseIdForLiteral(typename Solver::TLit lit) const {
-  return d_unitId.find(toInt(lit)) != d_unitId.end();
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::getClauseIdForLiteral(
-    typename Solver::TLit lit) const {
-  Assert(hasClauseIdForLiteral(lit));
-  return (*d_unitId.find(toInt(lit))).second;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::hasClauseRef(ClauseId id) const {
-  return d_idClause.find(id) != d_idClause.end();
-}
-
-template <class Solver>
-typename Solver::TCRef TSatProof<Solver>::getClauseRef(ClauseId id) const {
-  if (!hasClauseRef(id)) {
-    Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " "
-                       << ((d_deleted.find(id) != d_deleted.end()) ? "deleted"
-                                                                   : "")
-                       << (isUnit(id) ? "Unit" : "") << std::endl;
-  }
-  Assert(hasClauseRef(id));
-  return d_idClause.find(id)->second;
-}
-
-template <class Solver>
-const typename Solver::TClause& TSatProof<Solver>::getClause(
-    typename Solver::TCRef ref) const {
-  Assert(ref != Solver::TCRef_Undef);
-  Assert(ref >= 0 && ref < d_solver->ca.size());
-  return d_solver->ca[ref];
-}
-
-template <class Solver>
-void TSatProof<Solver>::getLitVec(ClauseId id, LitVector& vec) {
-  if (isUnit(id)) {
-    typename Solver::TLit lit = getUnit(id);
-    vec.push_back(lit);
-    return;
-  }
-  if (isAssumptionConflict(id)) {
-    vec = *(d_assumptionConflictsDebug[id]);
-    return;
-  }
-  typename Solver::TCRef cref = getClauseRef(id);
-  const typename Solver::TClause& cl = getClause(cref);
-  for (int i = 0; i < cl.size(); ++i) {
-    vec.push_back(cl[i]);
-  }
-}
-
-template <class Solver>
-bool TSatProof<Solver>::isUnit(ClauseId id) const {
-  return d_idUnit.find(id) != d_idUnit.end();
-}
-
-template <class Solver>
-typename Solver::TLit TSatProof<Solver>::getUnit(ClauseId id) const {
-  Assert(isUnit(id));
-  return (*d_idUnit.find(id)).second;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::isUnit(typename Solver::TLit lit) const {
-  return d_unitId.find(toInt(lit)) != d_unitId.end();
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::getUnitId(typename Solver::TLit lit) const {
-  Assert(isUnit(lit));
-  return (*d_unitId.find(toInt(lit))).second;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::hasResolutionChain(ClauseId id) const {
-  return d_resolutionChains.find(id) != d_resolutionChains.end();
-}
-
-template <class Solver>
-const typename TSatProof<Solver>::ResolutionChain&
-TSatProof<Solver>::getResolutionChain(ClauseId id) const {
-  Assert(hasResolutionChain(id));
-  const ResolutionChain* chain = (*d_resolutionChains.find(id)).second;
-  return *chain;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::isInputClause(ClauseId id) const {
-  return d_inputClauses.find(id) != d_inputClauses.end();
-}
-
-template <class Solver>
-bool TSatProof<Solver>::isLemmaClause(ClauseId id) const {
-  return d_lemmaClauses.find(id) != d_lemmaClauses.end();
-}
-
-template <class Solver>
-bool TSatProof<Solver>::isAssumptionConflict(ClauseId id) const {
-  return d_assumptionConflicts.find(id) != d_assumptionConflicts.end();
-}
-
-template <class Solver>
-void TSatProof<Solver>::print(ClauseId id) const {
-  if (d_deleted.find(id) != d_deleted.end()) {
-    Debug("proof:sat") << "del" << id;
-  } else if (isUnit(id)) {
-    printLit<Solver>(getUnit(id));
-  } else if (id == d_emptyClauseId) {
-    Debug("proof:sat") << "empty " << std::endl;
-  } else {
-    typename Solver::TCRef ref = getClauseRef(id);
-    printClause<Solver>(getClause(ref));
-  }
-}
-
-template <class Solver>
-void TSatProof<Solver>::printRes(ClauseId id) const {
-  Assert(hasResolutionChain(id));
-  Debug("proof:sat") << "id " << id << ": ";
-  printRes(getResolutionChain(id));
-}
-
-template <class Solver>
-void TSatProof<Solver>::printRes(const ResolutionChain& res) const {
-  ClauseId start_id = res.getStart();
-
-  if (Debug.isOn("proof:sat")) {
-    Debug("proof:sat") << "(";
-    print(start_id);
-  }
-
-  const typename ResolutionChain::ResSteps& steps = res.getSteps();
-  for (unsigned i = 0; i < steps.size(); i++) {
-    typename Solver::TLit v = steps[i].lit;
-    ClauseId id = steps[i].id;
-
-    if (Debug.isOn("proof:sat")) {
-      Debug("proof:sat") << "[";
-      printLit<Solver>(v);
-      Debug("proof:sat") << "] ";
-      print(id);
-    }
-  }
-  Debug("proof:sat") << ") \n";
-}
-
-/// registration methods
-template <class Solver>
-ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause,
-                                           ClauseKind kind) {
-  Assert(clause != Solver::TCRef_Undef);
-  typename ClauseIdMap::iterator it = d_clauseId.find(clause);
-  if (it == d_clauseId.end()) {
-    ClauseId newId = ProofManager::currentPM()->nextId();
-
-    d_clauseId.insert(std::make_pair(clause, newId));
-    d_idClause.insert(std::make_pair(newId, clause));
-    if (kind == INPUT) {
-      Assert(d_inputClauses.find(newId) == d_inputClauses.end());
-      d_inputClauses.insert(newId);
-    }
-    if (kind == THEORY_LEMMA) {
-      Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      d_lemmaClauses.insert(newId);
-      Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: "
-                       << newId << " = " << *buildClause(newId)
-                       << std::endl;
-    }
-  }
-
-  ClauseId id = d_clauseId[clause];
-  Assert(kind != INPUT || d_inputClauses.count(id));
-  Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id));
-
-  Debug("proof:sat:detailed") << "registerClause CRef: " << clause
-                              << " id: " << d_clauseId[clause]
-                              << "                kind: " << kind << "\n";
-  // ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] );
-  return id;
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit,
-                                               ClauseKind kind) {
-  Debug("cores") << "registerUnitClause " << kind << std::endl;
-  typename UnitIdMap::iterator it = d_unitId.find(toInt(lit));
-  if (it == d_unitId.end()) {
-    ClauseId newId = ProofManager::currentPM()->nextId();
-
-    if (d_unitId.find(toInt(lit)) == d_unitId.end())
-      d_unitId[toInt(lit)] = newId;
-    if (d_idUnit.find(newId) == d_idUnit.end())
-      d_idUnit[newId] = lit;
-
-    if (kind == INPUT) {
-      Assert(d_inputClauses.find(newId) == d_inputClauses.end());
-      Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new "
-                          "input (UNIT CLAUSE): "
-                       << lit << std::endl;
-      d_inputClauses.insert(newId);
-    }
-    if (kind == THEORY_LEMMA) {
-      Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): "
-                       << lit
-                       << std::endl;
-      d_lemmaClauses.insert(newId);
-    }
-  }
-  ClauseId id = d_unitId[toInt(lit)];
-  Assert(kind != INPUT || d_inputClauses.count(id));
-  Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id));
-  Debug("proof:sat:detailed") << "registerUnitClause id: " << id
-                              << " kind: " << kind << "\n";
-  // ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] );
-  return id;
-}
-template <class Solver>
-void TSatProof<Solver>::registerTrueLit(const typename Solver::TLit lit) {
-  Assert(d_trueLit == ClauseIdUndef);
-  d_trueLit = registerUnitClause(lit, INPUT);
-}
-
-template <class Solver>
-void TSatProof<Solver>::registerFalseLit(const typename Solver::TLit lit) {
-  Assert(d_falseLit == ClauseIdUndef);
-  d_falseLit = registerUnitClause(lit, INPUT);
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::getTrueUnit() const {
-  Assert(d_trueLit != ClauseIdUndef);
-  return d_trueLit;
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::getFalseUnit() const {
-  Assert(d_falseLit != ClauseIdUndef);
-  return d_falseLit;
-}
-
-template <class Solver>
-void TSatProof<Solver>::registerAssumption(const typename Solver::TVar var) {
-  Assert(d_assumptions.find(var) == d_assumptions.end());
-  d_assumptions.insert(var);
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::registerAssumptionConflict(
-    const typename Solver::TLitVec& confl) {
-  Debug("proof:sat:detailed") << "registerAssumptionConflict " << std::endl;
-  // Uniqueness is checked in the bit-vector proof
-  // should be vars
-  for (int i = 0; i < confl.size(); ++i) {
-    Assert(d_assumptions.find(var(confl[i])) != d_assumptions.end());
-  }
-  ClauseId new_id = ProofManager::currentPM()->nextId();
-  d_assumptionConflicts.insert(new_id);
-  LitVector* vec_confl = new LitVector(confl.size());
-  for (int i = 0; i < confl.size(); ++i) {
-    vec_confl->operator[](i) = confl[i];
-  }
-  if (Debug.isOn("proof:sat:detailed")) {
-    printClause<Solver>(*vec_confl);
-    Debug("proof:sat:detailed") << "\n";
-  }
-
-  d_assumptionConflictsDebug[new_id] = vec_confl;
-  return new_id;
-}
-
-template <class Solver>
-void TSatProof<Solver>::removedDfs(typename Solver::TLit lit,
-                                   LitSet* removedSet, LitVector& removeStack,
-                                   LitSet& inClause, LitSet& seen) {
-  // if we already added the literal return
-  if (seen.count(lit)) {
-    return;
-  }
-
-  typename Solver::TCRef reason_ref = d_solver->reason(var(lit));
-  if (reason_ref == Solver::TCRef_Undef) {
-    seen.insert(lit);
-    removeStack.push_back(lit);
-    return;
-  }
-
-  int size = getClause(reason_ref).size();
-  for (int i = 1; i < size; i++) {
-    typename Solver::TLit v = getClause(reason_ref)[i];
-    if (inClause.count(v) == 0 && seen.count(v) == 0) {
-      removedDfs(v, removedSet, removeStack, inClause, seen);
-    }
-  }
-  if (seen.count(lit) == 0) {
-    seen.insert(lit);
-    removeStack.push_back(lit);
-  }
-}
-
-template <class Solver>
-void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* res,
-                                               ClauseId id) {
-  LitSet* removed = res->getRedundant();
-  if (removed == NULL) {
-    return;
-  }
-
-  LitSet inClause;
-  createLitSet(id, inClause);
-
-  LitVector removeStack;
-  LitSet seen;
-  for (typename LitSet::iterator it = removed->begin(); it != removed->end();
-       ++it) {
-    removedDfs(*it, removed, removeStack, inClause, seen);
-  }
-
-  for (int i = removeStack.size() - 1; i >= 0; --i) {
-    typename Solver::TLit lit = removeStack[i];
-    typename Solver::TCRef reason_ref = d_solver->reason(var(lit));
-    ClauseId reason_id;
-
-    if (reason_ref == Solver::TCRef_Undef) {
-      Assert(isUnit(~lit));
-      reason_id = getUnitId(~lit);
-    } else {
-      reason_id = registerClause(reason_ref, LEARNT);
-    }
-    res->addStep(lit, reason_id, !sign(lit));
-  }
-  removed->clear();
-}
-
-template <class Solver>
-void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) {
-  Assert(res != NULL);
-
-  removeRedundantFromRes(res, id);
-  Assert(res->redundantRemoved());
-
-  // Because the SAT solver can add the same clause multiple times, it
-  // could be the case that a resolution chain for this clause already
-  // exists (e.g. when removing units in addClause).
-  if (hasResolutionChain(id)) {
-    ResChain<Solver>* current = (*d_resolutionChains.find(id)).second;
-    delete current;
-  }
-
-  d_resolutionChains.insert(id, res);
-
-  if (Debug.isOn("proof:sat")) {
-    printRes(id);
-  }
-  if (d_checkRes) {
-    Assert(checkResolution(id));
-  }
-
-}
-
-/// recording resolutions
-template <class Solver>
-void TSatProof<Solver>::startResChain(typename Solver::TCRef start) {
-  ClauseId id = getClauseIdForCRef(start);
-  ResolutionChain* res = new ResolutionChain(id);
-  d_resStack.push_back(res);
-}
-
-template <class Solver>
-void TSatProof<Solver>::startResChain(typename Solver::TLit start) {
-  ClauseId id = getUnitId(start);
-  ResolutionChain* res = new ResolutionChain(id);
-  d_resStack.push_back(res);
-}
-
-template <class Solver>
-void TSatProof<Solver>::addResolutionStep(typename Solver::TLit lit,
-                                          typename Solver::TCRef clause,
-                                          bool sign) {
-  ClauseId id = registerClause(clause, LEARNT);
-  ResChain<Solver>* res = d_resStack.back();
-  res->addStep(lit, id, sign);
-}
-
-template <class Solver>
-void TSatProof<Solver>::endResChain(ClauseId id) {
-  Debug("proof:sat:detailed") << "endResChain " << id << "\n";
-  Assert(d_resStack.size() > 0);
-  ResChain<Solver>* res = d_resStack.back();
-  registerResolution(id, res);
-  d_resStack.pop_back();
-}
-
-template <class Solver>
-void TSatProof<Solver>::endResChain(typename Solver::TLit lit) {
-  Assert(d_resStack.size() > 0);
-  ClauseId id = registerUnitClause(lit, LEARNT);
-  Debug("proof:sat:detailed") << "endResChain unit " << id << "\n";
-  ResolutionChain* res = d_resStack.back();
-  d_glueMap[id] = 1;
-  registerResolution(id, res);
-  d_resStack.pop_back();
-}
-
-template <class Solver>
-void TSatProof<Solver>::cancelResChain() {
-  Assert(d_resStack.size() > 0);
-  ResolutionChain* back = d_resStack.back();
-  delete back;
-  d_resStack.pop_back();
-}
-
-template <class Solver>
-void TSatProof<Solver>::storeLitRedundant(typename Solver::TLit lit) {
-  Assert(d_resStack.size() > 0);
-  ResolutionChain* res = d_resStack.back();
-  res->addRedundantLit(lit);
-}
-
-/// constructing resolutions
-template <class Solver>
-void TSatProof<Solver>::resolveOutUnit(typename Solver::TLit lit) {
-  ClauseId id = resolveUnit(~lit);
-  ResChain<Solver>* res = d_resStack.back();
-  res->addStep(lit, id, !sign(lit));
-}
-template <class Solver>
-void TSatProof<Solver>::storeUnitResolution(typename Solver::TLit lit) {
-  Debug("cores") << "STORE UNIT RESOLUTION" << std::endl;
-  resolveUnit(lit);
-}
-template <class Solver>
-ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) {
-  // first check if we already have a resolution for lit
-
-  if (isUnit(lit)) {
-    ClauseId id = getClauseIdForLiteral(lit);
-    Assert(hasResolutionChain(id) || isInputClause(id) || isLemmaClause(id));
-    return id;
-  }
-  typename Solver::TCRef reason_ref = d_solver->reason(var(lit));
-  Assert(reason_ref != Solver::TCRef_Undef);
-
-  ClauseId reason_id = registerClause(reason_ref, LEARNT);
-
-  ResChain<Solver>* res = new ResChain<Solver>(reason_id);
-  // Here, the call to resolveUnit() can reallocate memory in the
-  // clause allocator.  So reload reason ptr each time.
-  const typename Solver::TClause& initial_reason = getClause(reason_ref);
-  size_t current_reason_size = initial_reason.size();
-  for (size_t i = 0; i < current_reason_size; i++) {
-    const typename Solver::TClause& current_reason = getClause(reason_ref);
-    current_reason_size = current_reason.size();
-    typename Solver::TLit l = current_reason[i];
-    if (lit != l) {
-      ClauseId res_id = resolveUnit(~l);
-      res->addStep(l, res_id, !sign(l));
-    }
-  }
-  ClauseId unit_id = registerUnitClause(lit, LEARNT);
-  registerResolution(unit_id, res);
-  return unit_id;
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::storeUnitConflict(
-    typename Solver::TLit conflict_lit, ClauseKind kind) {
-  Debug("cores") << "STORE UNIT CONFLICT" << std::endl;
-  Assert(!d_unitConflictId.isSet());
-  d_unitConflictId.set(registerUnitClause(conflict_lit, kind));
-  Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId.get()
-                              << "\n";
-  return d_unitConflictId.get();
-}
-
-template <class Solver>
-void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
-  Assert(d_resStack.size() == 0);
-  Assert(conflict_ref != Solver::TCRef_Undef);
-  ClauseId conflict_id;
-  if (conflict_ref == Solver::TCRef_Lazy) {
-    Assert(d_unitConflictId.isSet());
-    conflict_id = d_unitConflictId.get();
-
-    ResChain<Solver>* res = new ResChain<Solver>(conflict_id);
-    typename Solver::TLit lit = d_idUnit[conflict_id];
-    ClauseId res_id = resolveUnit(~lit);
-    res->addStep(lit, res_id, !sign(lit));
-    registerResolution(d_emptyClauseId, res);
-    return;
-
-  } else {
-    Assert(!d_unitConflictId.isSet());
-    conflict_id = registerClause(conflict_ref, LEARNT);  // FIXME
-  }
-
-  if (Debug.isOn("proof:sat")) {
-    Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
-    print(conflict_id);
-    Debug("proof:sat") << std::endl;
-  }
-
-  ResChain<Solver>* res = new ResChain<Solver>(conflict_id);
-  // Here, the call to resolveUnit() can reallocate memory in the
-  // clause allocator.  So reload conflict ptr each time.
-  for (int i = 0; i < getClause(conflict_ref).size(); ++i) {
-    const typename Solver::TClause& conflict = getClause(conflict_ref);
-    typename Solver::TLit lit = conflict[i];
-    ClauseId res_id = resolveUnit(~lit);
-    res->addStep(lit, res_id, !sign(lit));
-  }
-
-  registerResolution(d_emptyClauseId, res);
-}
-
-/// CRef manager
-template <class Solver>
-void TSatProof<Solver>::updateCRef(typename Solver::TCRef oldref,
-                                   typename Solver::TCRef newref) {
-  if (d_clauseId.find(oldref) == d_clauseId.end()) {
-    return;
-  }
-  ClauseId id = getClauseIdForCRef(oldref);
-  Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end());
-  Assert(d_temp_idClause.find(id) == d_temp_idClause.end());
-  d_temp_clauseId[newref] = id;
-  d_temp_idClause[id] = newref;
-}
-
-template <class Solver>
-void TSatProof<Solver>::finishUpdateCRef() {
-  d_clauseId.swap(d_temp_clauseId);
-  d_temp_clauseId.clear();
-
-  d_idClause.swap(d_temp_idClause);
-  d_temp_idClause.clear();
-}
-
-template <class Solver>
-void TSatProof<Solver>::markDeleted(typename Solver::TCRef clause) {
-  if (hasClauseIdForCRef(clause)) {
-    ClauseId id = getClauseIdForCRef(clause);
-    Assert(d_deleted.find(id) == d_deleted.end());
-    d_deleted.insert(id);
-    if (isLemmaClause(id)) {
-      const typename Solver::TClause& minisat_cl = getClause(clause);
-      prop::SatClause* sat_cl = new prop::SatClause();
-      toSatClause<Solver>(minisat_cl, *sat_cl);
-      d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl));
-    }
-  }
-}
-
-template <class Solver>
-void TSatProof<Solver>::constructProof(ClauseId conflict) {
-  d_satProofConstructed = true;
-  collectClauses(conflict);
-}
-
-template <class Solver>
-void TSatProof<Solver>::refreshProof(ClauseId conflict) {
-  IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin();
-  IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end();
-
-  for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) {
-    if (d_deletedTheoryLemmas.find(seen_lemma_it->first) == d_deletedTheoryLemmas.end())
-      delete seen_lemma_it->second;
-  }
-
-  IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin();
-  IdToSatClause::const_iterator seen_input_end = d_seenInputs.end();
-
-  for (; seen_input_it != seen_input_end; ++seen_input_it) {
-    delete seen_input_it->second;
-  }
-
-  d_seenInputs.clear();
-  d_seenLemmas.clear();
-  d_seenLearnt.clear();
-
-  collectClauses(conflict);
-}
-
-template <class Solver>
-bool TSatProof<Solver>::proofConstructed() const {
-  return d_satProofConstructed;
-}
-
-template <class Solver>
-prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) {
-  if (isUnit(id)) {
-    typename Solver::TLit lit = getUnit(id);
-    prop::SatLiteral sat_lit = toSatLiteral<Solver>(lit);
-    prop::SatClause* clause = new prop::SatClause();
-    clause->push_back(sat_lit);
-    return clause;
-  }
-
-  if (isDeleted(id)) {
-    prop::SatClause* clause = d_deletedTheoryLemmas.find(id)->second;
-    return clause;
-  }
-
-  typename Solver::TCRef ref = getClauseRef(id);
-  const typename Solver::TClause& minisat_cl = getClause(ref);
-  prop::SatClause* clause = new prop::SatClause();
-  toSatClause<Solver>(minisat_cl, *clause);
-  return clause;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::derivedEmptyClause() const {
-  return hasResolutionChain(d_emptyClauseId);
-}
-
-template <class Solver>
-void TSatProof<Solver>::collectClauses(ClauseId id) {
-  if (d_seenInputs.find(id) != d_seenInputs.end() ||
-      d_seenLemmas.find(id) != d_seenLemmas.end() ||
-      d_seenLearnt.find(id) != d_seenLearnt.end()) {
-    return;
-  }
-
-  if (isInputClause(id)) {
-    d_seenInputs.insert(std::make_pair(id, buildClause(id)));
-    return;
-  } else if (isLemmaClause(id)) {
-    d_seenLemmas.insert(std::make_pair(id, buildClause(id)));
-    return;
-  } else if (!isAssumptionConflict(id)) {
-    d_seenLearnt.insert(id);
-  }
-
-  const ResolutionChain& res = getResolutionChain(id);
-  const typename ResolutionChain::ResSteps& steps = res.getSteps();
-  ClauseId start = res.getStart();
-  collectClauses(start);
-
-  for (size_t i = 0; i < steps.size(); i++) {
-    collectClauses(steps[i].id);
-  }
-}
-
-template <class Solver>
-void TSatProof<Solver>::collectClausesUsed(IdToSatClause& inputs,
-                                           IdToSatClause& lemmas) {
-  inputs = d_seenInputs;
-  lemmas = d_seenLemmas;
-}
-
-template <class Solver>
-void TSatProof<Solver>::storeClauseGlue(ClauseId clause, int glue) {
-  Assert(d_glueMap.find(clause) == d_glueMap.end());
-  d_glueMap.insert(std::make_pair(clause, glue));
-}
-
-template <class Solver>
-TSatProof<Solver>::Statistics::Statistics(const std::string& prefix)
-    : d_numLearnedClauses(
-        smtStatisticsRegistry().registerInt(prefix + "NumLearnedClauses")),
-      d_numLearnedInProof(
-          smtStatisticsRegistry().registerInt(prefix + "NumLearnedInProof")),
-      d_numLemmasInProof(
-          smtStatisticsRegistry().registerInt(prefix + "NumLemmasInProof")),
-      d_avgChainLength(smtStatisticsRegistry().registerAverage(
-          prefix + "AvgResChainLength")),
-      d_resChainLengths(smtStatisticsRegistry().registerHistogram<uint64_t>(
-          prefix + "ResChainLengthsHist")),
-      d_usedResChainLengths(smtStatisticsRegistry().registerHistogram<uint64_t>(
-          prefix + "UsedResChainLengthsHist")),
-      d_clauseGlue(smtStatisticsRegistry().registerHistogram<uint64_t>(
-          prefix + "ClauseGlueHist")),
-      d_usedClauseGlue(smtStatisticsRegistry().registerHistogram<uint64_t>(
-          prefix + "UsedClauseGlueHist"))
-{
-}
-
-inline std::ostream& operator<<(std::ostream& out, cvc5::ClauseKind k)
-{
-  switch (k) {
-    case cvc5::INPUT: out << "INPUT"; break;
-    case cvc5::THEORY_LEMMA: out << "THEORY_LEMMA"; break;
-    case cvc5::LEARNT: out << "LEARNT"; break;
-    default:
-      out << "ClauseKind Unknown! [" << unsigned(k) << "]";
-  }
-
-  return out;
-}
-
-}  // namespace cvc5
-
-#endif /* CVC5__SAT__PROOF_IMPLEMENTATION_H */
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 0fb4a59b5..f8a34ec42 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -22,9 +22,6 @@
 #include "expr/node.h"
 #include "options/bv_options.h"
 #include "proof/clause_id.h"
-#include "proof/cnf_proof.h"
-#include "proof/proof_manager.h"
-#include "proof/sat_proof.h"
 #include "prop/minisat/minisat.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
@@ -54,7 +51,6 @@ CnfStream::CnfStream(SatSolver* satSolver,
       d_flitPolicy(flpol),
       d_registrar(registrar),
       d_name(name),
-      d_cnfProof(nullptr),
       d_removable(false),
       d_resourceManager(rm)
 {
@@ -86,10 +82,6 @@ bool CnfStream::assertClause(TNode node, SatClause& c)
 
   ClauseId clauseId = d_satSolver->addClause(c, d_removable);
 
-  if (d_cnfProof && clauseId != ClauseIdUndef)
-  {
-    d_cnfProof->registerConvertedClause(clauseId);
-  }
   return clauseId != ClauseIdUndef;
 }
 
@@ -159,27 +151,11 @@ void CnfStream::ensureLiteral(TNode n)
     // If we were called with something other than a theory atom (or
     // Boolean variable), we get a SatLiteral that is definitionally
     // equal to it.
-    //
-    // We are setting the current assertion to be null. This is because `toCNF`
-    // may add clauses to the SAT solver and we look up the current assertion
-    // in that case. Setting it to null ensures that the assertion stack is
-    // 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.
-    if (d_cnfProof)
-    {
-      d_cnfProof->pushCurrentAssertion(Node::null());
-    }
     // These are not removable and have no proof ID
     d_removable = false;
 
     SatLiteral lit = toCNF(n, false);
 
-    if (d_cnfProof)
-    {
-      d_cnfProof->popCurrentAssertion();
-    }
-
     // Store backward-mappings
     // These may already exist
     d_literalToNodeMap.insert_safe(lit, n);
@@ -239,7 +215,6 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister
   if (preRegister) {
     // In case we are re-entered due to lemmas, save our state
     bool backupRemovable = d_removable;
-    // Should be fine since cnfProof current assertion is stack based.
     d_registrar->preRegister(node);
     d_removable = backupRemovable;
   }
@@ -277,11 +252,6 @@ bool CnfStream::isNotifyFormula(TNode node) const
   return d_notifyFormulas.find(node) != d_notifyFormulas.end();
 }
 
-void CnfStream::setProof(CnfProof* proof) {
-  Assert(d_cnfProof == NULL);
-  d_cnfProof = proof;
-}
-
 SatLiteral CnfStream::convertAtom(TNode node)
 {
   Trace("cnf") << "convertAtom(" << node << ")\n";
@@ -737,17 +707,7 @@ void CnfStream::convertAndAssert(TNode node,
                << ", negated = " << (negated ? "true" : "false")
                << ", removable = " << (removable ? "true" : "false") << ")\n";
   d_removable = removable;
-
-  if (d_cnfProof)
-  {
-    d_cnfProof->pushCurrentAssertion(negated ? node.notNode() : (Node)node,
-                                     input);
-  }
   convertAndAssert(node, negated);
-  if (d_cnfProof)
-  {
-    d_cnfProof->popCurrentAssertion();
-  }
 }
 
 void CnfStream::convertAndAssert(TNode node, bool negated)
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 9901fb18b..264e26777 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -30,7 +30,6 @@
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "proof/proof_manager.h"
 #include "prop/proof_cnf_stream.h"
 #include "prop/registrar.h"
 #include "prop/sat_solver_types.h"
@@ -164,8 +163,6 @@ class CnfStream {
   /** Retrieves map from literals to nodes. */
   const CnfStream::LiteralToNodeMap& getNodeCache() const;
 
-  void setProof(CnfProof* proof);
-
  protected:
   /**
    * Same as above, except that uses the saved d_removable flag. It calls the
@@ -243,9 +240,6 @@ class CnfStream {
   /** The name of this CNF stream*/
   std::string d_name;
 
-  /** Pointer to the proof corresponding to this CnfStream */
-  CnfProof* d_cnfProof;
-
   /**
    * Are we asserting a removable clause (true) or a permanent clause (false).
    * This is set at the beginning of convertAndAssert so that it doesn't
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 971fb95d2..41019d58e 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -31,10 +31,6 @@ 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"
 #include "prop/minisat/minisat.h"
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/theory_proxy.h"
@@ -228,10 +224,6 @@ Solver::Solver(cvc5::prop::TheoryProxy* proxy,
     d_pfManager.reset(
         new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
   }
-  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-  {
-    ProofManager::currentPM()->initSatProof(this);
-  }
 
   // Create the constant variables
   varTrue = newVar(true, false, false);
@@ -240,12 +232,6 @@ Solver::Solver(cvc5::prop::TheoryProxy* proxy,
   // Assert the constants
   uncheckedEnqueue(mkLit(varTrue, false));
   uncheckedEnqueue(mkLit(varFalse, true));
-  // FIXME: these should be axioms I believe
-  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-  {
-    ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
-    ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
-  }
 }
 
 
@@ -423,24 +409,6 @@ CRef Solver::reason(Var x) {
 
     // Construct the reason
     CRef real_reason = ca.alloc(explLevel, explanation, true);
-    // FIXME: at some point will need more information about where this explanation
-    // came from (ie. the theory/sharing)
-    Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)"
-                     << std::endl;
-    if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-    {
-      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);
@@ -514,14 +482,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
       lemmas.push();
       ps.copyTo(lemmas.last());
       lemmas_removable.push(removable);
-      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-      {
-        // 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);
 
@@ -533,22 +493,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           // construct the clause below to give to the proof manager
           // as the final conflict.
           if(falseLiteralsCount == 1) {
-            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-            {
-              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(
-                  cvc5::Minisat::CRef_Lazy);
-            }
             if (needProof())
             {
               d_pfManager->finalizeProof(ps[0], true);
@@ -576,26 +520,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
         if (options::unsatCores() || needProof())
         {
-          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-          {
-            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)
           {
-            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-            {
-              ProofManager::getSatProof()->finalizeProof(cr);
-            }
             if (needProof())
             {
               d_pfManager->finalizeProof(ca[cr], true);
@@ -614,20 +540,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
                          << std::endl;
           if (ps.size() == 1)
           {
-            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-            {
-              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);
-              }
-            }
             // We need to do this so that the closedness check, if being done,
             // goes through when we have unit assumptions whose literal has
             // already been registered, as the ProofCnfStream will not register
@@ -640,20 +552,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           CRef confl = propagate(CHECK_WITHOUT_THEORY);
           if(! (ok = (confl == CRef_Undef)) ) {
-            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-            {
-              if (ca[confl].size() == 1)
-              {
-                id = ProofManager::getSatProof()->storeUnitConflict(
-                    ca[confl][0], LEARNT);
-                ProofManager::getSatProof()->finalizeProof(
-                    cvc5::Minisat::CRef_Lazy);
-              }
-              else
-              {
-                ProofManager::getSatProof()->finalizeProof(confl);
-              }
-            }
             if (needProof())
             {
               if (ca[confl].size() == 1)
@@ -668,10 +566,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           return ok;
         } else {
-          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-          {
-            id = ClauseIdUndef;
-          }
           return ok;
         }
       }
@@ -715,10 +609,6 @@ void Solver::detachClause(CRef cr, bool strict) {
       Debug("minisat") << "\n";
     }
     Assert(c.size() > 1);
-    if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-    {
-      ProofManager::getSatProof()->markDeleted(cr);
-    }
 
     if (strict){
         remove(watches[~c[0]], Watcher(cr, c[1]));
@@ -997,10 +887,6 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 
   int max_resolution_level = 0;  // Maximal level of the resolved clauses
 
-  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-  {
-    ProofManager::getSatProof()->startResChain(confl);
-    }
     if (needProof())
     {
       d_pfManager->startResChain(ca[confl]);
@@ -1059,17 +945,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 (level(var(q)) == 0 && needProof())
             {
-              if (options::unsatCoresMode()
-                  == options::UnsatCoresMode::OLD_PROOF)
-              {
-                ProofManager::getSatProof()->resolveOutUnit(q);
-              }
-              if (needProof())
-              {
-                d_pfManager->addResolutionStep(q);
-              }
+              d_pfManager->addResolutionStep(q);
             }
           }
         }
@@ -1082,19 +960,12 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
         seen[var(p)] = 0;
         pathC--;
 
-        if (pathC > 0 && confl != CRef_Undef)
+        if (pathC > 0 && confl != CRef_Undef && needProof())
         {
-          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-          {
-            ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
-          }
-          if (needProof())
-          {
-            d_pfManager->addResolutionStep(ca[confl], p);
-          }
+          d_pfManager->addResolutionStep(ca[confl], p);
         }
 
-    }while (pathC > 0);
+    } while (pathC > 0);
     out_learnt[0] = ~p;
     if (Debug.isOn("newproof::sat"))
     {
@@ -1124,11 +995,6 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                 // Literal is not redundant
                 out_learnt[j++] = out_learnt[i];
               } else {
-                if (options::unsatCoresMode()
-                    == options::UnsatCoresMode::OLD_PROOF)
-                {
-                  ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
-                }
                 if (needProof())
                 {
                   Debug("newproof::sat")
@@ -1419,12 +1285,6 @@ void Solver::propagateTheory() {
         MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
         ClauseId id; // FIXME: mark it as explanation here somehow?
         addClause(explanation, true, id);
-        // explainPropagation() pushes the explanation on the assertion
-        // stack in CnfProof, so we need to pop it here.
-        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-        {
-          ProofManager::getCnfProof()->popCurrentAssertion();
-        }
       }
     }
   }
@@ -1565,12 +1425,6 @@ void Solver::removeSatisfied(vec<CRef>& cs)
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
         if (satisfied(c)) {
-          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
-              && locked(c))
-          {
-            // store a resolution of the literal c propagated
-            ProofManager::getSatProof()->storeUnitResolution(c[0]);
-          }
           removeClause(cs[i]);
         }
         else
@@ -1673,10 +1527,6 @@ lbool Solver::search(int nof_conflicts)
 
       if (decisionLevel() == 0)
       {
-        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-        {
-          ProofManager::getSatProof()->finalizeProof(confl);
-        }
         if (needProof())
         {
           if (confl == CRef_Lazy)
@@ -1700,10 +1550,6 @@ lbool Solver::search(int nof_conflicts)
       if (learnt_clause.size() == 1)
       {
         uncheckedEnqueue(learnt_clause[0]);
-        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-        {
-          ProofManager::getSatProof()->endResChain(learnt_clause[0]);
-        }
         if (needProof())
         {
           d_pfManager->endResChain(learnt_clause[0]);
@@ -1718,11 +1564,6 @@ lbool Solver::search(int nof_conflicts)
         attachClause(cr);
         claBumpActivity(ca[cr]);
         uncheckedEnqueue(learnt_clause[0], cr);
-        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-        {
-          ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
-          ProofManager::getSatProof()->endResChain(id);
-        }
         if (needProof())
         {
           d_pfManager->endResChain(ca[cr]);
@@ -2059,12 +1900,7 @@ void Solver::relocAll(ClauseAllocator& to)
             vec<Watcher>& ws = watches[p];
             for (int j = 0; j < ws.size(); j++)
             {
-              ca.reloc(ws[j].cref,
-                       to,
-                       options::unsatCoresMode()
-                               == options::UnsatCoresMode::OLD_PROOF
-                           ? ProofManager::getSatProof()
-                           : nullptr);
+              ca.reloc(ws[j].cref, to);
             }
         }
 
@@ -2076,37 +1912,20 @@ void Solver::relocAll(ClauseAllocator& to)
         if (hasReasonClause(v)
             && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
         {
-          ca.reloc(
-              vardata[v].d_reason,
-              to,
-              options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
-                  ? ProofManager::getSatProof()
-                  : nullptr);
+          ca.reloc(vardata[v].d_reason, to);
         }
     }
     // All learnt:
     //
     for (int i = 0; i < clauses_removable.size(); i++)
     {
-      ca.reloc(clauses_removable[i],
-               to,
-               options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
-                   ? ProofManager::getSatProof()
-                   : nullptr);
+      ca.reloc(clauses_removable[i], to);
     }
     // All original:
     //
     for (int i = 0; i < clauses_persistent.size(); i++)
     {
-      ca.reloc(clauses_persistent[i],
-               to,
-               options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
-                   ? ProofManager::getSatProof()
-                   : nullptr);
-    }
-    if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-    {
-      ProofManager::getSatProof()->finishUpdateCRef();
+      ca.reloc(clauses_persistent[i], to);
     }
 }
 
@@ -2249,9 +2068,6 @@ CRef Solver::updateLemmas() {
   // Last index in the trail
   int backtrack_index = trail.size();
 
-  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
-         || lemmas.size() == static_cast<int>(lemmas_cnf_assertion.size()));
-
   // Attach all the clauses and enqueue all the propagations
   for (int j = 0; j < lemmas.size(); ++j)
   {
@@ -2274,16 +2090,6 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-      {
-        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 {
@@ -2295,17 +2101,6 @@ CRef Solver::updateLemmas() {
     // If the lemma is propagating enqueue its literal (or set the conflict)
     if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
       if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
-        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
-            && lemma.size() == 1)
-        {
-          Node cnf_assertion = lemmas_cnf_assertion[j];
-
-          Trace("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);
-        }
         Trace("pf::sat") << "Solver::updateLemmas: unit theory lemma: "
                          << lemma[0] << std::endl;
         if (value(lemma[0]) == l_False) {
@@ -2316,10 +2111,6 @@ CRef Solver::updateLemmas() {
           } else {
             Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
             conflict = CRef_Lazy;
-            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-            {
-              ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
-            }
             if (needProof())
             {
               d_pfManager->storeUnitConflict(lemma[0]);
@@ -2334,11 +2125,8 @@ CRef Solver::updateLemmas() {
     }
   }
 
-  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
-         || lemmas.size() == static_cast<int>(lemmas_cnf_assertion.size()));
   // Clear the lemmas
   lemmas.clear();
-  lemmas_cnf_assertion.clear();
   lemmas_removable.clear();
 
   if (conflict != CRef_Undef) {
@@ -2350,24 +2138,17 @@ CRef Solver::updateLemmas() {
   return conflict;
 }
 
-void ClauseAllocator::reloc(CRef& cr,
-                            ClauseAllocator& to,
-                            cvc5::TSatProof<Solver>* proof)
+void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to)
 {
   Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl;
   // FIXME what is this CRef_lazy
   if (cr == CRef_Lazy) return;
 
-  CRef old = cr;  // save the old reference
   Clause& c = operator[](cr);
   if (c.reloced()) { cr = c.relocation(); return; }
 
   cr = to.alloc(c.level(), c, c.removable());
   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?)
   to[cr].mark(c.mark());
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index f4aa04e4d..bed637904 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -39,7 +39,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "util/resource_manager.h"
 
 namespace cvc5 {
-template <class Solver> class TSatProof;
 
 namespace prop {
 class PropEngine;
@@ -58,7 +57,6 @@ class Solver {
   friend class cvc5::prop::PropEngine;
   friend class cvc5::prop::TheoryProxy;
   friend class cvc5::prop::SatProofManager;
-  friend class cvc5::TSatProof<Minisat::Solver>;
 
  public:
   static CRef TCRef_Undef;
@@ -103,9 +101,6 @@ class Solver {
   /** Is the lemma removable */
   vec<bool> lemmas_removable;
 
-  /** Nodes being converted to CNF */
-  std::vector<cvc5::Node> lemmas_cnf_assertion;
-
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
 
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 312d0b6de..405d97a56 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -33,14 +33,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 namespace cvc5 {
 namespace Minisat {
-class Solver;
-}
-template <class Solver>
-class TSatProof;
-}  // namespace cvc5
 
-namespace cvc5 {
-namespace Minisat {
+class Solver;
 
 //=================================================================================================
 // Variables, literals, lifted booleans, clauses:
@@ -320,9 +314,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
     }
 
-    void reloc(CRef& cr,
-               ClauseAllocator& to,
-               cvc5::TSatProof<Solver>* proof = NULL);
+    void reloc(CRef& cr, ClauseAllocator& to);
     // Implementation moved to Solver.cc.
 };
 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 293e7175b..4adbbe7f7 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -22,7 +22,6 @@
 #include "options/prop_options.h"
 #include "options/smt_options.h"
 #include "proof/clause_id.h"
-#include "proof/sat_proof.h"
 #include "prop/minisat/simp/SimpSolver.h"
 #include "util/statistics_stats.h"
 
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 0e6ca28b8..15ef5cacb 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -22,6 +22,14 @@
 #include "util/statistics_registry.h"
 
 namespace cvc5 {
+
+template <class Solver>
+prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
+
+template <class Solver>
+void toSatClause(const typename Solver::TClause& minisat_cl,
+                 prop::SatClause& sat_cl);
+
 namespace prop {
 
 class MinisatSatSolver : public CDCLTSatSolverInterface
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index b71c728e7..bcf75b43a 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -29,7 +29,6 @@
 #include "options/options.h"
 #include "options/proof_options.h"
 #include "options/smt_options.h"
-#include "proof/proof_manager.h"
 #include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
 #include "prop/prop_proof_manager.h"
@@ -132,10 +131,6 @@ PropEngine::PropEngine(TheoryEngine* te,
     d_ppm.reset(
         new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
   }
-  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-  {
-    ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
-  }
 }
 
 void PropEngine::finishInit()
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index b764695cc..605c75a14 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -21,7 +21,6 @@
 #include "decision/decision_engine.h"
 #include "options/decision_options.h"
 #include "options/smt_options.h"
-#include "proof/cnf_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/skolem_def_manager.h"
@@ -105,10 +104,6 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
            || tte.getGenerator());
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }
-  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-  {
-    ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
-  }
   Debug("prop-explain") << "explainPropagation() => " << theoryExplanation
                         << std::endl;
   explanation.push_back(l);
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 7dc2e915d..504dce71e 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -23,7 +23,6 @@
 #include "options/expr_options.h"
 #include "options/language.h"
 #include "options/smt_options.h"
-#include "proof/proof_manager.h"
 #include "smt/abstract_values.h"
 #include "smt/env.h"
 #include "smt/smt_engine.h"
@@ -193,25 +192,6 @@ void Assertions::addFormula(TNode n,
     }
   }
 
-  // Give it to the old proof manager
-  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
-  {
-    if (inInput)
-    {  // n is an input assertion
-      if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores()
-          || options::checkUnsatCores())
-      {
-        ProofManager::currentPM()->addCoreAssertion(n);
-      }
-    }
-    else
-    {
-      // n is the result of an unknown preprocessing step, add it to dependency
-      // map to null
-      ProofManager::currentPM()->addDependence(n, Node::null());
-    }
-  }
-
   // Add the normalized formula to the queue
   d_assertions.push_back(n, isAssumption, true);
 }
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index be19923af..e7870e4d7 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -104,8 +104,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // set proofs on if not yet set
-  if (options::unsatCores() && !options::produceProofs()
-      && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF)
+  if (options::unsatCores() && !options::produceProofs())
   {
     if (opts.wasSetByUser(options::produceProofs))
     {
@@ -318,7 +317,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   // new unsat core specific restrictions for proofs
   if (options::unsatCores()
-      && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
       && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
   {
     // no fine-graininess
@@ -413,12 +411,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.set(options::produceAssertions, true);
   }
 
-  // whether we want to force safe unsat cores, i.e., if we are in the OLD_PROOF
-  // unsat core mode or ASSUMPTIONS, the new default, since other ones are
-  // experimental
+  // whether we want to force safe unsat cores, i.e., if we are in the default
+  // ASSUMPTIONS mode, since other ones are experimental
   bool safeUnsatCores =
-      options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
-      || options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS;
+      options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS;
 
   // Disable options incompatible with incremental solving, unsat cores or
   // output an error if enabled explicitly. It is also currently incompatible
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0e1ff8878..bd38f630d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -33,7 +33,6 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"
-#include "proof/proof_manager.h"
 #include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
 #include "smt/abduction_solver.h"
@@ -91,7 +90,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
       d_routListener(new ResourceOutListener(*this)),
       d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
       d_smtSolver(nullptr),
-      d_proofManager(nullptr),
       d_model(nullptr),
       d_checkModels(nullptr),
       d_pfManager(nullptr),
@@ -140,15 +138,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // make the quantifier elimination solver
   d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver));
 
-  // The ProofManager is constructed before any other proof objects such as
-  // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
-  // initialized in TheoryEngine and PropEngine respectively.
-  Assert(d_proofManager == nullptr);
-
-  // d_proofManager must be created before Options has been finished
-  // being parsed from the input file. Because of this, we cannot trust
-  // that d_env->getOption(options::unsatCores) is set correctly yet.
-  d_proofManager.reset(new ProofManager(getUserContext()));
 }
 
 bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); }
@@ -317,15 +306,6 @@ SmtEngine::~SmtEngine()
     //destroy all passes before destroying things that they refer to
     d_pp->cleanup();
 
-    // d_proofManager is always created when proofs are enabled at configure
-    // time.  Because of this, this code should not be wrapped in PROOF() which
-    // additionally checks flags such as
-    // d_env->getOption(options::produceProofs).
-    //
-    // Note: the proof manager must be destroyed before the theory engine.
-    // Because the destruction of the proofs depends on contexts owned be the
-    // theory solvers.
-    d_proofManager.reset(nullptr);
     d_pfManager.reset(nullptr);
     d_ucManager.reset(nullptr);
 
@@ -1403,12 +1383,6 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
         "Cannot get an unsat core unless immediately preceded by "
         "UNSAT/ENTAILED response.");
   }
-  // use old proof infrastructure
-  if (!d_pfManager)
-  {
-    d_proofManager->traceUnsatCore();  // just to trigger core creation
-    return UnsatCore(d_proofManager->extractUnsatCore());
-  }
   // generate with new proofs
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 924e3c974..b8cd1c3d7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -41,7 +41,6 @@ class TypeNode;
 class Env;
 class NodeManager;
 class TheoryEngine;
-class ProofManager;
 class UnsatCore;
 class LogicRequest;
 class StatisticsRegistry;
@@ -99,7 +98,6 @@ class SmtScope;
 class PfManager;
 class UnsatCoreManager;
 
-ProofManager* currentProofManager();
 }  // namespace smt
 
 /* -------------------------------------------------------------------------- */
@@ -858,12 +856,6 @@ class CVC5_EXPORT SmtEngine
   /** Get a pointer to the PropEngine owned by this SmtEngine. */
   prop::PropEngine* getPropEngine();
 
-  /**
-   * Get a pointer to the ProofManager owned by this SmtEngine.
-   * TODO (project #37): this is the old proof manager and will be deleted
-   */
-  ProofManager* getProofManager() { return d_proofManager.get(); };
-
   /** Get the resource manager of this SMT engine */
   ResourceManager* getResourceManager() const;
 
@@ -1076,8 +1068,6 @@ class CVC5_EXPORT SmtEngine
   /** The SMT solver */
   std::unique_ptr<smt::SmtSolver> d_smtSolver;
 
-  /** The (old) proof manager TODO (project #37): delete this */
-  std::unique_ptr<ProofManager> d_proofManager;
   /**
    * The SMT-level model object, which contains information about how to
    * print the model, as well as a pointer to the underlying TheoryModel
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 962529924..98f4c8d70 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -35,11 +35,6 @@ SmtEngine* currentSmtEngine() {
 
 bool smtEngineInScope() { return s_smtEngine_current != NULL; }
 
-ProofManager* currentProofManager() {
-  Assert(s_smtEngine_current != NULL);
-  return s_smtEngine_current->getProofManager();
-}
-
 ResourceManager* currentResourceManager()
 {
   return s_smtEngine_current->getResourceManager();
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 76bc5c641..cc231fa3c 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -27,7 +27,6 @@
 
 namespace cvc5 {
 
-class ProofManager;
 class SmtEngine;
 class StatisticsRegistry;
 
@@ -36,9 +35,6 @@ namespace smt {
 SmtEngine* currentSmtEngine();
 bool smtEngineInScope();
 
-// FIXME: Maybe move into SmtScope?
-ProofManager* currentProofManager();
-
 /** get the current resource manager */
 ResourceManager* currentResourceManager();
 
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 34ef53194..eaf5cf82f 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -23,7 +23,6 @@
 #include "expr/term_context_stack.h"
 #include "expr/term_conversion_proof_generator.h"
 #include "options/smt_options.h"
-#include "proof/proof_manager.h"
 
 using namespace std;
 
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 0415d4271..9effdbec7 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -21,7 +21,6 @@
 #include "options/printer_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
-#include "proof/proof_manager.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp
index e53b1ed13..a3bdf10ad 100644
--- a/src/theory/quantifiers/quantifiers_macros.cpp
+++ b/src/theory/quantifiers/quantifiers_macros.cpp
@@ -18,7 +18,6 @@
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
-#include "proof/proof_manager.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/quantifiers_registry.h"
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index d83c326c7..c0f1805ff 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -19,7 +19,6 @@
 #include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
-#include "proof/proof_manager.h"
 #include "smt/logic_exception.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/strings/arith_entail.h"
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 7124a8890..8885abe6b 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -20,7 +20,6 @@
 
 #include "base/output.h"
 #include "options/smt_options.h"
-#include "proof/proof_manager.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/uf/eq_proof.h"