Bit vector proof superclass (#2599)

* Split BitvectorProof into a sub/superclass

The superclass contains general printing knowledge.

The subclass contains CNF or Resolution-specific knowledge.

* Renames & code moves

* Nits cleaned in prep for PR

* Moved CNF-proof from ResolutionBitVectorProof to BitVectorProof

Since DRAT BV proofs will also contain a CNF-proof, the CNF proof should
be stored in `BitVectorProof`.

* Unique pointers, comments, and code movement.

Adjusted the distribution of code between BVP and RBVP.
  Notably, put the CNF proof in BVP because it isn't
  resolution-specific.
Added comments to the headers of both files -- mostly BVP.
Changed two owned pointers into unique_ptr.
  BVP's pointer to a CNF proof
  RBVP's pointer to a resolution proof

BVP: `BitVectorProof`
RBVP: `ResolutionBitVectorProof`

* clang-format

* Undo manual copyright modification

* s/superclass/base class/

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* make LFSCBitVectorProof::printOwnedSort public

* Andres's Comments

Mostly cleaning up (or trying to clean up) includes.

* Cleaned up one header cycle

However, this only allowed me to move the forward-decl, not eliminate
it, because there were actually two underlying include cycles that the
forward-decl solved.

* Added single _s to header gaurds

* Fix Class name in debug output

Credits to Andres

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* Reordered methods in BitVectorProof per original  ordering

7 files changed, 921 insertions, 550 deletions

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 8f001ffa1..c9e98d170 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -9,31 +9,19 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** [[ Add lengthier description here ]]
-
- ** \todo document this file
-
-**/
+ ** Contains implementions (e.g. code for printing bitblasting bindings that is
+ ** common to all kinds of bitvector proofs.
+ **/
 
 #include "proof/bitvector_proof.h"
 #include "options/bv_options.h"
 #include "options/proof_options.h"
-#include "proof/array_proof.h"
-#include "proof/clause_id.h"
-#include "proof/lfsc_proof_printer.h"
 #include "proof/proof_output_channel.h"
-#include "proof/proof_utils.h"
-#include "proof/sat_proof_implementation.h"
-#include "prop/bvminisat/bvminisat.h"
+#include "proof/theory_proof.h"
 #include "theory/bv/bitblast/bitblaster.h"
 #include "theory/bv/theory_bv.h"
-#include "theory/bv/theory_bv_rewrite_rules.h"
-
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
 
 namespace CVC4 {
-
 BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv,
                                TheoryProofEngine* proofEngine)
     : TheoryProof(bv, proofEngine),
@@ -41,73 +29,44 @@ BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv,
       d_seenBBTerms(),
       d_bbTerms(),
       d_bbAtoms(),
-      d_resolutionProof(NULL),
-      d_cnfProof(NULL),
-      d_isAssumptionConflict(false),
-      d_bitblaster(NULL),
-      d_useConstantLetification(false) {}
-
-void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) {
-  Assert (d_resolutionProof == NULL);
-  d_resolutionProof = new BVSatProof(solver, &d_fakeContext, "bb", true);
-}
-
-theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; }
-void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
-                                  context::Context* cnf) {
-  Assert (d_resolutionProof != NULL);
-  Assert (d_cnfProof == NULL);
-  d_cnfProof = new LFSCCnfProof(cnfStream, cnf, "bb");
-
-  // 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->pushCurrentDefinition(true_node);
-  d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit());
-  d_cnfProof->popCurrentAssertion();
-  d_cnfProof->popCurrentDefinition();
-
-  d_cnfProof->pushCurrentAssertion(false_node);
-  d_cnfProof->pushCurrentDefinition(false_node);
-  d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit());
-  d_cnfProof->popCurrentAssertion();
-  d_cnfProof->popCurrentDefinition();
+      d_bitblaster(nullptr),
+      d_useConstantLetification(false),
+      d_cnfProof()
+{
 }
 
-void BitVectorProof::setBitblaster(bv::TBitblaster<Node>* bb) {
-  Assert (d_bitblaster == NULL);
+void BitVectorProof::setBitblaster(theory::bv::TBitblaster<Node>* bb)
+{
+  Assert(d_bitblaster == NULL);
   d_bitblaster = bb;
 }
 
-BVSatProof* BitVectorProof::getSatProof() {
-  Assert (d_resolutionProof != NULL);
-  return d_resolutionProof;
-}
-
-void BitVectorProof::registerTermBB(Expr term) {
-  Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term << " )" << std::endl;
+void BitVectorProof::registerTermBB(Expr term)
+{
+  Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term
+                  << " )" << std::endl;
 
-  if (d_seenBBTerms.find(term) != d_seenBBTerms.end())
-    return;
+  if (d_seenBBTerms.find(term) != d_seenBBTerms.end()) return;
 
   d_seenBBTerms.insert(term);
   d_bbTerms.push_back(term);
 
-  // If this term gets used in the final proof, we will want to register it. However,
-  // we don't know this at this point; and when the theory proof engine sees it, if it belongs
-  // to another theory, it won't register it with this proof. So, we need to tell the
-  // engine to inform us.
+  // If this term gets used in the final proof, we will want to register it.
+  // However, we don't know this at this point; and when the theory proof engine
+  // sees it, if it belongs to another theory, it won't register it with this
+  // proof. So, we need to tell the engine to inform us.
 
-  if (theory::Theory::theoryOf(term) != theory::THEORY_BV) {
-    Debug("pf::bv") << "\tMarking term " << term << " for future BV registration" << std::endl;
+  if (theory::Theory::theoryOf(term) != theory::THEORY_BV)
+  {
+    Debug("pf::bv") << "\tMarking term " << term
+                    << " for future BV registration" << std::endl;
     d_proofEngine->markTermForFutureRegistration(term, theory::THEORY_BV);
   }
 }
 
 void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) {
-  Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom << ", " << atom_bb << " )" << std::endl;
+  Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom
+                  << ", " << atom_bb << " )" << std::endl;
 
   Expr def = atom.iffExpr(atom_bb);
   d_bbAtoms.insert(std::make_pair(atom, def));
@@ -119,7 +78,8 @@ void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) {
 }
 
 void BitVectorProof::registerTerm(Expr term) {
-  Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl;
+  Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )"
+                  << std::endl;
 
   if (options::lfscLetification() && term.isConst()) {
     if (d_constantLetMap.find(term) == d_constantLetMap.end()) {
@@ -131,8 +91,8 @@ void BitVectorProof::registerTerm(Expr term) {
 
   d_usedBB.insert(term);
 
-  if (Theory::isLeafOf(term, theory::THEORY_BV) &&
-      !term.isConst()) {
+  if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst())
+  {
     d_declarations.insert(term);
   }
 
@@ -147,149 +107,32 @@ void BitVectorProof::registerTerm(Expr term) {
   }
 }
 
-std::string BitVectorProof::getBBTermName(Expr expr) {
-  Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" << expr.getId() << std::endl;
+std::string BitVectorProof::getBBTermName(Expr expr)
+{
+  Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt"
+                  << expr.getId() << std::endl;
   std::ostringstream os;
-  os << "bt"<< expr.getId();
+  os << "bt" << expr.getId();
   return os.str();
 }
 
-void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TCRef cr) {
-  d_resolutionProof->startResChain(cr);
-}
-
-void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TLit lit) {
-  d_resolutionProof->startResChain(lit);
-}
-
-void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl) {
-  Debug("pf::bv") << "BitVectorProof::endBVConflict called" << std::endl;
-
-  std::vector<Expr> expr_confl;
-  for (int i = 0; i < confl.size(); ++i) {
-    prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]);
-    Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr();
-    Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
-    expr_confl.push_back(expr_lit);
-  }
-
-  Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl);
-  Debug("pf::bv") << "Make conflict for " << conflict << std::endl;
-
-  if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) {
-    Debug("pf::bv") << "Abort...already conflict for " << conflict << std::endl;
-    // This can only happen when we have eager explanations in the bv solver
-    // if we don't get to propagate p before ~p is already asserted
-    d_resolutionProof->cancelResChain();
-    return;
-  }
-
-  // we don't need to check for uniqueness in the sat solver then
-  ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl);
-  d_bbConflictMap[conflict] = clause_id;
-  d_resolutionProof->endResChain(clause_id);
-  Debug("pf::bv") << "BitVectorProof::endBVConflict id" <<clause_id<< " => " << conflict << "\n";
-  d_isAssumptionConflict = false;
-}
-
-void BitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) {
-
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    Debug("pf::bv") << "Construct full proof." << std::endl;
-    d_resolutionProof->constructProof();
-    return;
-  }
-
-  for (unsigned i = 0; i < conflicts.size(); ++i) {
-    Expr confl = conflicts[i];
-    Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl;
-
-    // Special case: if the conflict has a (true) or a (not false) in it, it is trivial...
-    bool ignoreConflict = false;
-    if ((confl.isConst() && confl.getConst<bool>()) ||
-        (confl.getKind() == kind::NOT && confl[0].isConst() && !confl[0].getConst<bool>())) {
-      ignoreConflict = true;
-    } else if (confl.getKind() == kind::OR) {
-      for (unsigned k = 0; k < confl.getNumChildren(); ++k) {
-        if ((confl[k].isConst() && confl[k].getConst<bool>()) ||
-            (confl[k].getKind() == kind::NOT && confl[k][0].isConst() && !confl[k][0].getConst<bool>())) {
-          ignoreConflict = true;
-        }
-      }
-    }
-    if (ignoreConflict) {
-      Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)" << std::endl;
-      continue;
-    }
-
-    if (d_bbConflictMap.find(confl) != d_bbConflictMap.end()) {
-      ClauseId id = d_bbConflictMap[confl];
-      d_resolutionProof->collectClauses(id);
-    } else {
-      // There is no exact match for our conflict, but maybe it is a subset of another conflict
-      ExprToClauseId::const_iterator it;
-      bool matchFound = false;
-      for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
-        Expr possibleMatch = it->first;
-        if (possibleMatch.getKind() != kind::OR) {
-          // This is a single-node conflict. If this node is in the conflict we're trying to prove,
-          // we have a match.
-          for (unsigned k = 0; k < confl.getNumChildren(); ++k) {
-            if (confl[k] == possibleMatch) {
-              matchFound = true;
-              d_resolutionProof->collectClauses(it->second);
-              break;
-            }
-          }
-        } else {
-          if (possibleMatch.getNumChildren() > confl.getNumChildren())
-            continue;
-
-          unsigned k = 0;
-          bool matching = true;
-          for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) {
-            // j is the index in possibleMatch
-            // k is the index in confl
-            while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) {
-              ++k;
-            }
-            if (k == confl.getNumChildren()) {
-              // We couldn't find a match for possibleMatch[j], so not a match
-              matching = false;
-              break;
-            }
-          }
-
-          if (matching) {
-            Debug("pf::bv") << "Collecting info from a sub-conflict" << std::endl;
-            d_resolutionProof->collectClauses(it->second);
-            matchFound = true;
-            break;
-          }
-        }
-      }
-
-      if (!matchFound) {
-        Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl
-                        << "Dumping existing conflicts:" << std::endl;
-
-        i = 0;
-        for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
-          ++i;
-          Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl;
-        }
-
-        Unreachable();
-      }
-    }
-  }
+void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
+                                  context::Context* cnf)
+{
+  Assert(d_cnfProof == nullptr);
+  d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb"));
 }
 
-void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
-  Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedTerm( " << term << " ), theory is: "
-                  << Theory::theoryOf(term) << std::endl;
+void BitVectorProof::printOwnedTerm(Expr term,
+                                    std::ostream& os,
+                                    const ProofLetMap& map)
+{
+  Debug("pf::bv") << std::endl
+                  << "(pf::bv) BitVectorProof::printOwnedTerm( " << term
+                  << " ), theory is: " << theory::Theory::theoryOf(term)
+                  << std::endl;
 
-  Assert (Theory::theoryOf(term) == THEORY_BV);
+  Assert(theory::Theory::theoryOf(term) == theory::THEORY_BV);
 
   // peel off eager bit-blasting trick
   if (term.getKind() == kind::BITVECTOR_EAGER_ATOM) {
@@ -380,21 +223,24 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const Proof
   }
 }
 
-void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const ProofLetMap& map) {
+void BitVectorProof::printBitOf(Expr term,
+                                std::ostream& os,
+                                const ProofLetMap& map)
+{
   Assert (term.getKind() == kind::BITVECTOR_BITOF);
   unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex;
   Expr var = term[0];
 
-  Debug("pf::bv") << "LFSCBitVectorProof::printBitOf( " << term << " ), "
-                  << "bit = " << bit
-                  << ", var = " << var << std::endl;
+  Debug("pf::bv") << "BitVectorProof::printBitOf( " << term << " ), "
+                  << "bit = " << bit << ", var = " << var << std::endl;
 
   os << "(bitof ";
   os << d_exprToVariableName[var];
   os << " " << bit << ")";
 }
 
-void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) {
+void BitVectorProof::printConstant(Expr term, std::ostream& os)
+{
   Assert (term.isConst());
   os << "(a_bv " << utils::getSize(term) << " ";
 
@@ -413,7 +259,10 @@ void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) {
   }
 }
 
-void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) {
+void BitVectorProof::printOperatorNary(Expr term,
+                                       std::ostream& os,
+                                       const ProofLetMap& map)
+{
   std::string op = utils::toLFSCKindTerm(term);
   std::ostringstream paren;
   std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : "";
@@ -431,7 +280,10 @@ void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const Pr
   }
 }
 
-void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) {
+void BitVectorProof::printOperatorUnary(Expr term,
+                                        std::ostream& os,
+                                        const ProofLetMap& map)
+{
   os <<"(";
   os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" ";
   os << " ";
@@ -439,7 +291,10 @@ void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const P
   os <<")";
 }
 
-void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) {
+void BitVectorProof::printPredicate(Expr term,
+                                    std::ostream& os,
+                                    const ProofLetMap& map)
+{
   os <<"(";
   os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term[0]) <<" ";
   os << " ";
@@ -449,7 +304,10 @@ void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const Proof
   os <<")";
 }
 
-void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) {
+void BitVectorProof::printOperatorParametric(Expr term,
+                                             std::ostream& os,
+                                             const ProofLetMap& map)
+{
   os <<"(";
   os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" ";
   os <<" ";
@@ -477,185 +335,25 @@ void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, co
   os <<")";
 }
 
-void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) {
-  Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl;
+void BitVectorProof::printOwnedSort(Type type, std::ostream& os)
+{
+  Debug("pf::bv") << std::endl
+                  << "(pf::bv) BitVectorProof::printOwnedSort( " << type << " )"
+                  << std::endl;
   Assert (type.isBitVector());
   unsigned width = utils::getSize(type);
   os << "(BitVec " << width << ")";
 }
 
-void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
-  Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" << std::endl;
-  Expr conflict = utils::mkSortedExpr(kind::OR, lemma);
-  Debug("pf::bv") << "\tconflict = " << conflict << std::endl;
-
-  if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) {
-    std::ostringstream lemma_paren;
-    for (unsigned i = 0; i < lemma.size(); ++i) {
-      Expr lit = lemma[i];
-
-      if (lit.getKind() == kind::NOT) {
-        os << "(intro_assump_t _ _ _ ";
-      } else {
-        os << "(intro_assump_f _ _ _ ";
-      }
-      lemma_paren <<")";
-      // print corresponding literal in main sat solver
-      ProofManager* pm = ProofManager::currentPM();
-      CnfProof* cnf = pm->getCnfProof();
-      prop::SatLiteral main_lit = cnf->getLiteral(lit);
-      os << pm->getLitName(main_lit);
-      os <<" ";
-      // print corresponding literal in bv sat solver
-      prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
-      os << pm->getAtomName(bb_var, "bb");
-      os <<"(\\ unit"<<bb_var<<"\n";
-      lemma_paren <<")";
-    }
-    Expr lem = utils::mkOr(lemma);
-    Assert (d_bbConflictMap.find(lem) != d_bbConflictMap.end());
-    ClauseId lemma_id = d_bbConflictMap[lem];
-    proof::LFSCProofPrinter::printAssumptionsResolution(
-        d_resolutionProof, lemma_id, os, lemma_paren);
-    os <<lemma_paren.str();
-  } else {
-
-    Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching sub-conflict..."
-                    << std::endl;
-
-    bool matching;
-
-    ExprToClauseId::const_iterator it;
-    unsigned i = 0;
-    for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
-      // Our conflict is sorted, and the records are also sorted.
-      ++i;
-      Expr possibleMatch = it->first;
-
-      if (possibleMatch.getKind() != kind::OR) {
-        // This is a single-node conflict. If this node is in the conflict we're trying to prove,
-        // we have a match.
-        matching = false;
-
-        for (unsigned k = 0; k < conflict.getNumChildren(); ++k) {
-          if (conflict[k] == possibleMatch) {
-            matching = true;
-            break;
-          }
-        }
-      } else {
-        if (possibleMatch.getNumChildren() > conflict.getNumChildren())
-          continue;
-
-        unsigned k = 0;
-
-        matching = true;
-        for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) {
-          // j is the index in possibleMatch
-          // k is the index in conflict
-          while (k < conflict.getNumChildren() && conflict[k] != possibleMatch[j]) {
-            ++k;
-          }
-          if (k == conflict.getNumChildren()) {
-            // We couldn't find a match for possibleMatch[j], so not a match
-            matching = false;
-            break;
-          }
-        }
-      }
-
-      if (matching) {
-        Debug("pf::bv") << "Found a match with conflict #" << i << ": " << std::endl << possibleMatch << std::endl;
-        // The rest is just a copy of the usual handling, if a precise match is found.
-        // We only use the literals that appear in the matching conflict, though, and not in the
-        // original lemma - as these may not have even been bit blasted!
-        std::ostringstream lemma_paren;
-
-        if (possibleMatch.getKind() == kind::OR) {
-          for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) {
-            Expr lit = possibleMatch[i];
-
-            if (lit.getKind() == kind::NOT) {
-              os << "(intro_assump_t _ _ _ ";
-            } else {
-              os << "(intro_assump_f _ _ _ ";
-            }
-            lemma_paren <<")";
-            // print corresponding literal in main sat solver
-            ProofManager* pm = ProofManager::currentPM();
-            CnfProof* cnf = pm->getCnfProof();
-            prop::SatLiteral main_lit = cnf->getLiteral(lit);
-            os << pm->getLitName(main_lit);
-            os <<" ";
-            // print corresponding literal in bv sat solver
-            prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
-            os << pm->getAtomName(bb_var, "bb");
-            os <<"(\\ unit"<<bb_var<<"\n";
-            lemma_paren <<")";
-          }
-        } else {
-          // The conflict only consists of one node, either positive or negative.
-          Expr lit = possibleMatch;
-          if (lit.getKind() == kind::NOT) {
-            os << "(intro_assump_t _ _ _ ";
-          } else {
-            os << "(intro_assump_f _ _ _ ";
-          }
-          lemma_paren <<")";
-          // print corresponding literal in main sat solver
-          ProofManager* pm = ProofManager::currentPM();
-          CnfProof* cnf = pm->getCnfProof();
-          prop::SatLiteral main_lit = cnf->getLiteral(lit);
-          os << pm->getLitName(main_lit);
-          os <<" ";
-          // print corresponding literal in bv sat solver
-          prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
-          os << pm->getAtomName(bb_var, "bb");
-          os <<"(\\ unit"<<bb_var<<"\n";
-          lemma_paren <<")";
-        }
-
-        ClauseId lemma_id = it->second;
-        proof::LFSCProofPrinter::printAssumptionsResolution(
-            d_resolutionProof, lemma_id, os, lemma_paren);
-        os <<lemma_paren.str();
-
-        return;
-      }
-    }
-
-    // We failed to find a matching sub conflict. The last hope is that the
-    // conflict has a FALSE assertion in it; this can happen in some corner cases,
-    // where the FALSE is the result of a rewrite.
-
-    for (unsigned i = 0; i < lemma.size(); ++i) {
-      if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse()) {
-        Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl;
-        os << "(clausify_false ";
-        os << ProofManager::getLitName(lemma[i]);
-        os << ")";
-        return;
-      }
-    }
-
-    Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl
-                    << "Dumping existing conflicts:" << std::endl;
-
-    i = 0;
-    for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
-      ++i;
-      Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl;
-    }
-
-    Unreachable();
-  }
-}
-
-void LFSCBitVectorProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
+void BitVectorProof::printSortDeclarations(std::ostream& os,
+                                           std::ostream& paren)
+{
   // Nothing to do here at this point.
 }
 
-void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
+void BitVectorProof::printTermDeclarations(std::ostream& os,
+                                           std::ostream& paren)
+{
   ExprSet::const_iterator it = d_declarations.begin();
   ExprSet::const_iterator end = d_declarations.end();
   for (; it != end; ++it) {
@@ -671,7 +369,9 @@ void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& p
   }
 }
 
-void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
+void BitVectorProof::printDeferredDeclarations(std::ostream& os,
+                                               std::ostream& paren)
+{
   if (options::lfscLetification()) {
     os << std::endl << ";; BV const letification\n" << std::endl;
     std::map<Expr,std::string>::const_iterator it;
@@ -694,7 +394,10 @@ void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostrea
   }
 }
 
-void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
+void BitVectorProof::printAliasingDeclarations(std::ostream& os,
+                                               std::ostream& paren,
+                                               const ProofLetMap& globalLetMap)
+{
   // Print "trust" statements to bind complex bv variables to their associated terms
 
   ExprToString::const_iterator it = d_assignedAliases.begin();
@@ -720,13 +423,15 @@ void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostrea
   os << "\n";
 }
 
-void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
+void BitVectorProof::printTermBitblasting(Expr term, std::ostream& os)
+{
   // TODO: once we have the operator elimination rules remove those that we
   // eliminated
   Assert (term.getType().isBitVector());
   Kind kind = term.getKind();
 
-  if (Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) {
+  if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst())
+  {
     // A term is a leaf if it has no children, or if it belongs to another theory
     os << "(bv_bbl_var " << utils::getSize(term) << " " << d_exprToVariableName[term];
     os << " _)";
@@ -857,12 +562,14 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
     return;
   }
 
-  default:
-    Unreachable("LFSCBitVectorProof Unknown operator");
+  default: Unreachable("BitVectorProof Unknown operator");
   }
 }
 
-void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) {
+void BitVectorProof::printAtomBitblasting(Expr atom,
+                                          std::ostream& os,
+                                          bool swap)
+{
   Kind kind = atom.getKind();
   switch(kind) {
   case kind::BITVECTOR_ULT :
@@ -888,12 +595,12 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool
 
     return;
   }
-  default:
-    Unreachable("LFSCBitVectorProof Unknown atom kind");
+  default: Unreachable("BitVectorProof Unknown atom kind");
   }
 }
 
-void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) {
+void BitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os)
+{
   Assert(atom.getKind() == kind::EQUAL);
 
   os << "(bv_bbl_=_false";
@@ -907,10 +614,13 @@ void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os
   os << ")";
 }
 
-void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) {
+void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
+{
   // bit-blast terms
   {
-    Debug("pf::bv") << "LFSCBitVectorProof::printBitblasting: the bitblasted terms are: " << std::endl;
+    Debug("pf::bv")
+        << "BitVectorProof::printBitblasting: the bitblasted terms are: "
+        << std::endl;
     std::vector<Expr>::const_iterator it = d_bbTerms.begin();
     std::vector<Expr>::const_iterator end = d_bbTerms.end();
 
@@ -999,52 +709,13 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
   }
 }
 
-void LFSCBitVectorProof::calculateAtomsInBitblastingProof() {
-  // Collect the input clauses used
-  IdToSatClause used_lemmas;
-  IdToSatClause used_inputs;
-  d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
-  d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof);
-  Assert(used_lemmas.empty());
-}
-
-const std::set<Node>* LFSCBitVectorProof::getAtomsInBitblastingProof() {
+const std::set<Node>* BitVectorProof::getAtomsInBitblastingProof()
+{
   return &d_atomsInBitblastingProof;
 }
 
-void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
-                                              std::ostream& paren,
-                                              ProofLetMap& letMap) {
-  // print mapping between theory atoms and internal SAT variables
-  os << std::endl << ";; BB atom mapping\n" << std::endl;
-
-  std::set<Node>::iterator atomIt;
-  Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl;
-  for (atomIt = d_atomsInBitblastingProof.begin(); atomIt != d_atomsInBitblastingProof.end(); ++atomIt) {
-    Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl;
-  }
-  Debug("pf::bv") << std::endl;
-
-  // first print bit-blasting
-  printBitblasting(os, paren);
-
-  // print CNF conversion proof for bit-blasted facts
-  IdToSatClause used_lemmas;
-  IdToSatClause used_inputs;
-  d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
-
-  d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
-  os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl;
-  for (IdToSatClause::iterator it = used_inputs.begin();
-       it != used_inputs.end(); ++it) {
-    d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren);
-  }
-
-  os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl;
-  proof::LFSCProofPrinter::printResolutions(d_resolutionProof, os, paren);
-}
-
-std::string LFSCBitVectorProof::assignAlias(Expr expr) {
+std::string BitVectorProof::assignAlias(Expr expr)
+{
   Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end());
 
   std::stringstream ss;
@@ -1054,11 +725,14 @@ std::string LFSCBitVectorProof::assignAlias(Expr expr) {
   return ss.str();
 }
 
-bool LFSCBitVectorProof::hasAlias(Expr expr) {
+bool BitVectorProof::hasAlias(Expr expr)
+{
   return d_assignedAliases.find(expr) != d_assignedAliases.end();
 }
 
-void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
+void BitVectorProof::printConstantDisequalityProof(
+    std::ostream& os, Expr c1, Expr c2, const ProofLetMap& globalLetMap)
+{
   Assert (c1.isConst());
   Assert (c2.isConst());
   Assert (utils::getSize(c1) == utils::getSize(c2));
@@ -1088,7 +762,10 @@ void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1
   os << ")";
 }
 
-void LFSCBitVectorProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) {
+void BitVectorProof::printRewriteProof(std::ostream& os,
+                                       const Node& n1,
+                                       const Node& n2)
+{
   ProofLetMap emptyMap;
   os << "(rr_bv_default ";
   d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap);
@@ -1097,4 +774,4 @@ void LFSCBitVectorProof::printRewriteProof(std::ostream& os, const Node &n1, con
   os << ")";
 }
 
-} /* namespace CVC4 */
+}  // namespace CVC4
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 63f1cdf63..466efa6a7 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -9,118 +9,166 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Bitvector proof
+ ** \brief Bitvector proof base class
  **
- ** Bitvector proof
+ ** Contains code (e.g. proof printing code) which is common to all bitvector
+ *proofs.
  **/
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__BITVECTOR__PROOF_H
-#define __CVC4__BITVECTOR__PROOF_H
+#ifndef __CVC4__BITVECTOR_PROOF_H
+#define __CVC4__BITVECTOR_PROOF_H
 
-#include <iostream>
 #include <set>
-#include <sstream>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
-
 #include "expr/expr.h"
+#include "proof/cnf_proof.h"
 #include "proof/theory_proof.h"
-#include "prop/bvminisat/core/Solver.h"
-
+#include "theory/bv/bitblast/bitblaster.h"
+#include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
 
-namespace prop {
-class CnfStream;
-} /* namespace CVC4::prop */
-
-namespace theory {
-namespace bv {
-class TheoryBV;
-template <class T> class TBitblaster;
-} /* namespace CVC4::theory::bv */
-} /* namespace CVC4::theory */
-
-class CnfProof;
-} /* namespace CVC4 */
-
-namespace CVC4 {
-
-template <class Solver> class TSatProof;
-typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof;
-
 typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
 typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
 typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
 typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr;
 typedef std::unordered_map<Expr, std::string, ExprHashFunction> ExprToString;
 
-class BitVectorProof : public TheoryProof {
-protected:
+/**
+ * A bitvector proof is best understood as having
+ *
+ *    1. A declaration of a "bitblasted formulas" -- boolean formulas
+ *       that are each translations of a BV-literal (a comparison between BVs).
+ *
+ *       (and a proof that each "bitblasted formula" is implied by the
+ *       corresponding BV literal)
+ *
+ *    2. A declaration of a cnf formula equisatisfiable to the bitblasted
+ *       formula
+ *
+ *       (and a proof that each clause is implied by some bitblasted formula)
+ *
+ *    3. A proof of UNSAT from the clauses.
+ *
+ * This class is responsible for 1 & 2. The proof of UNSAT is delegated to a
+ * subclass.
+ */
+class BitVectorProof : public TheoryProof
+{
+ protected:
+  BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
+  virtual ~BitVectorProof(){};
+
+  // Set of BV variables in the input. (e.g. "a" in [ a = 000 ] ^ [ a == 001 ])
   ExprSet d_declarations;
 
-  ExprSet d_usedBB; // terms and formulas that are actually relevant to the proof
+  // terms and formulas that are actually relevant to the proof
+  ExprSet d_usedBB;
+
+  ExprSet d_seenBBTerms;        // terms that need to be bit-blasted
+  std::vector<Expr> d_bbTerms;  // order of bit-blasting
 
-  ExprSet d_seenBBTerms; // terms that need to be bit-blasted
-  std::vector<Expr> d_bbTerms; // order of bit-blasting
-  ExprToExpr d_bbAtoms; // atoms that need to be bit-blasted
+  /** atoms that need to be bit-blasted,
+   * BV-literals -> (BV-literals <=> bool formula)
+   * where a BV literal is a signed or unsigned comparison.
+   */
+  ExprToExpr d_bbAtoms;
 
   // map from Expr representing normalized lemma to ClauseId in SAT solver
   ExprToClauseId d_bbConflictMap;
-  BVSatProof* d_resolutionProof;
 
-  CnfProof* d_cnfProof;
-
-  bool d_isAssumptionConflict;
   theory::bv::TBitblaster<Node>* d_bitblaster;
+
+  /** In an LFSC proof the manifestation of this expression bit-level
+   * representation will have a string name. This method returns that name.
+   */
   std::string getBBTermName(Expr expr);
 
-  std::map<Expr,std::string> d_constantLetMap;
+  /** A mapping from constant BV terms to identifiers that will refer to them in
+   * an LFSC proof, if constant-letification is enabled.
+   */
+  std::map<Expr, std::string> d_constantLetMap;
+
+  /** Should we introduced identifiers to refer to BV constant terms?  It may
+   * reduce the textual size of a proof!
+   */
   bool d_useConstantLetification;
-  theory::TheoryId getTheoryId() override;
-  context::Context d_fakeContext;
-public:
-  BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
 
-  void initSatProof(CVC4::BVMinisat::Solver* solver);
-  void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx);
-  void setBitblaster(theory::bv::TBitblaster<Node>* bb);
+  /** Temporary storage for the set of nodes in the bitblasted formula which
+   * correspond to CNF variables eventually used in the proof of unsat on the
+   * CNF formula
+   */
+  std::set<Node> d_atomsInBitblastingProof;
 
-  BVSatProof* getSatProof();
-  CnfProof* getCnfProof() {return d_cnfProof; }
-  void finalizeConflicts(std::vector<Expr>& conflicts);
+  /**
+   * Prints out
+   *   (a) a declaration of bit-level interpretations corresponding to bits in
+   *       the input BV terms.
+   *   (b) a proof that the each BV literal entails a boolean formula on
+   *       bitof expressions.
+   */
+  void printBitblasting(std::ostream& os, std::ostream& paren);
 
-  void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
-  void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
   /**
-   * All the
-   *
-   * @param confl an inconsistent set of bv literals
+   * The proof that the bit-blasted SAT formula is correctly converted to CNF
    */
-  void endBVConflict(const BVMinisat::Solver::TLitVec& confl);
-  void markAssumptionConflict() { d_isAssumptionConflict = true; }
-  bool isAssumptionConflict() { return d_isAssumptionConflict; }
+  std::unique_ptr<CnfProof> d_cnfProof;
+
+ public:
+  void printOwnedTerm(Expr term,
+                      std::ostream& os,
+                      const ProofLetMap& map) override;
+
+  void printOwnedSort(Type type, std::ostream& os) override;
+
+  /**
+   * Populate the d_atomsInBitblastingProof member.
+   * See its documentation
+   */
+  virtual void calculateAtomsInBitblastingProof() = 0;
+
+  /**
+   * Read the d_atomsInBitblastingProof member.
+   * See its documentation.
+   */
+  const std::set<Node>* getAtomsInBitblastingProof();
 
   void registerTermBB(Expr term);
+
+  /**
+   * Informs the proof that the `atom` predicate was bitblasted into the
+   * `atom_bb` term.
+   *
+   * The `atom` term must be a comparison of bitvectors, and the `atom_bb` term
+   * a boolean formula on bitof expressions
+   */
   void registerAtomBB(Expr atom, Expr atom_bb);
 
   void registerTerm(Expr term) override;
 
-  virtual void printTermBitblasting(Expr term, std::ostream& os) = 0;
-  virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0;
-  virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0;
+  /**
+   * This must be done before registering any terms or atoms, since the CNF
+   * proof must reflect the result of bitblasting those
+   */
+  virtual void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx);
 
-  virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0;
-  virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0;
-  virtual const std::set<Node>* getAtomsInBitblastingProof() = 0;
-  virtual void calculateAtomsInBitblastingProof() = 0;
-};
+  CnfProof* getCnfProof() { return d_cnfProof.get(); }
+
+  void setBitblaster(theory::bv::TBitblaster<Node>* bb);
 
-class LFSCBitVectorProof: public BitVectorProof {
+ private:
+  ExprToString d_exprToVariableName;
+
+  ExprToString d_assignedAliases;
+  std::map<std::string, std::string> d_aliasToBindDeclaration;
+  std::string assignAlias(Expr expr);
+  bool hasAlias(Expr expr);
 
+  // Functions for printing various BV terms. Helpers for BV's `printOwnedTerm`
   void printConstant(Expr term, std::ostream& os);
   void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map);
   void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map);
@@ -128,29 +176,19 @@ class LFSCBitVectorProof: public BitVectorProof {
   void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map);
   void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map);
 
-  ExprToString d_exprToVariableName;
-  ExprToString d_assignedAliases;
-  std::map<std::string, std::string> d_aliasToBindDeclaration;
-  std::string assignAlias(Expr expr);
-  bool hasAlias(Expr expr);
+  /**
+   * Prints the LFSC construction of a bblast_term for `term`
+   */
+  void printTermBitblasting(Expr term, std::ostream& os);
 
-  std::set<Node> d_atomsInBitblastingProof;
+  /**
+   * For a given BV-atom (a comparison), prints a proof that that comparison
+   * holds iff the bitblasted equivalent of it holds.
+   * Uses a side-condidition to do the bit-blasting.
+   */
+  void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
+  void printAtomBitblastingToFalse(Expr term, std::ostream& os);
 
-public:
-  LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
-    :BitVectorProof(bv, proofEngine)
-  {}
-  void printOwnedTerm(Expr term,
-                      std::ostream& os,
-                      const ProofLetMap& map) override;
-  void printOwnedSort(Type type, std::ostream& os) override;
-  void printTermBitblasting(Expr term, std::ostream& os) override;
-  void printAtomBitblasting(Expr term, std::ostream& os, bool swap) override;
-  void printAtomBitblastingToFalse(Expr term, std::ostream& os) override;
-  void printTheoryLemmaProof(std::vector<Expr>& lemma,
-                             std::ostream& os,
-                             std::ostream& paren,
-                             const ProofLetMap& map) override;
   void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
   void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
   void printDeferredDeclarations(std::ostream& os,
@@ -158,12 +196,7 @@ public:
   void printAliasingDeclarations(std::ostream& os,
                                  std::ostream& paren,
                                  const ProofLetMap& globalLetMap) override;
-  void printBitblasting(std::ostream& os, std::ostream& paren) override;
-  void printResolutionProof(std::ostream& os,
-                            std::ostream& paren,
-                            ProofLetMap& letMap) override;
-  void calculateAtomsInBitblastingProof() override;
-  const std::set<Node>* getAtomsInBitblastingProof() override;
+
   void printConstantDisequalityProof(std::ostream& os,
                                      Expr c1,
                                      Expr c2,
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index e7b00068a..5b26432dd 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -21,11 +21,11 @@
 #include "context/context.h"
 #include "options/bv_options.h"
 #include "options/proof_options.h"
-#include "proof/bitvector_proof.h"
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/proof_utils.h"
+#include "proof/resolution_bitvector_proof.h"
 #include "proof/sat_proof_implementation.h"
 #include "proof/theory_proof.h"
 #include "smt/smt_engine.h"
@@ -116,10 +116,11 @@ UFProof* ProofManager::getUfProof() {
   return (UFProof*)pf;
 }
 
-BitVectorProof* ProofManager::getBitVectorProof() {
+proof::ResolutionBitVectorProof* ProofManager::getBitVectorProof()
+{
   Assert (options::proof());
   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV);
-  return (BitVectorProof*)pf;
+  return static_cast<proof::ResolutionBitVectorProof*>(pf);
 }
 
 ArrayProof* ProofManager::getArrayProof() {
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 0342288fe..82efbab0f 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -69,7 +69,10 @@ class TheoryProof;
 class UFProof;
 class ArithProof;
 class ArrayProof;
-class BitVectorProof;
+
+namespace proof {
+class ResolutionBitVectorProof;
+}
 
 template <class Solver> class LFSCSatProof;
 typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof;
@@ -77,7 +80,6 @@ typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof;
 class LFSCCnfProof;
 class LFSCTheoryProofEngine;
 class LFSCUFProof;
-class LFSCBitVectorProof;
 class LFSCRewriterProof;
 
 namespace prop {
@@ -189,7 +191,7 @@ public:
   static TheoryProofEngine* getTheoryProofEngine();
   static TheoryProof* getTheoryProof( theory::TheoryId id );
   static UFProof* getUfProof();
-  static BitVectorProof* getBitVectorProof();
+  static proof::ResolutionBitVectorProof* getBitVectorProof();
   static ArrayProof* getArrayProof();
   static ArithProof* getArithProof();
 
diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp
new file mode 100644
index 000000000..667d630f8
--- /dev/null
+++ b/src/proof/resolution_bitvector_proof.cpp
@@ -0,0 +1,522 @@
+/*********************                                                        */
+/*! \file resolution_bitvector_proof.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Guy Katz, Paul Meng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+ ** \todo document this file
+
+**/
+
+#include "proof/resolution_bitvector_proof.h"
+#include "options/bv_options.h"
+#include "options/proof_options.h"
+#include "proof/array_proof.h"
+#include "proof/bitvector_proof.h"
+#include "proof/clause_id.h"
+#include "proof/lfsc_proof_printer.h"
+#include "proof/proof_output_channel.h"
+#include "proof/proof_utils.h"
+#include "proof/sat_proof_implementation.h"
+#include "prop/bvminisat/bvminisat.h"
+#include "theory/bv/bitblast/bitblaster.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_rewrite_rules.h"
+
+#include <iostream>
+#include <sstream>
+
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
+namespace CVC4 {
+
+namespace proof {
+
+ResolutionBitVectorProof::ResolutionBitVectorProof(
+    theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+    : BitVectorProof(bv, proofEngine),
+      d_resolutionProof(),
+      d_isAssumptionConflict(false)
+{
+}
+
+void ResolutionBitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver)
+{
+  Assert(d_resolutionProof == NULL);
+  d_resolutionProof.reset(new BVSatProof(solver, &d_fakeContext, "bb", true));
+}
+
+theory::TheoryId ResolutionBitVectorProof::getTheoryId()
+{
+  return theory::THEORY_BV;
+}
+
+void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
+                                            context::Context* cnf)
+{
+  Assert(d_resolutionProof != NULL);
+  BitVectorProof::initCnfProof(cnfStream, cnf);
+
+  // 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->pushCurrentDefinition(true_node);
+  d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit());
+  d_cnfProof->popCurrentAssertion();
+  d_cnfProof->popCurrentDefinition();
+
+  d_cnfProof->pushCurrentAssertion(false_node);
+  d_cnfProof->pushCurrentDefinition(false_node);
+  d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit());
+  d_cnfProof->popCurrentAssertion();
+  d_cnfProof->popCurrentDefinition();
+}
+
+BVSatProof* ResolutionBitVectorProof::getSatProof()
+{
+  Assert(d_resolutionProof != NULL);
+  return d_resolutionProof.get();
+}
+
+void ResolutionBitVectorProof::startBVConflict(
+    CVC4::BVMinisat::Solver::TCRef cr)
+{
+  d_resolutionProof->startResChain(cr);
+}
+
+void ResolutionBitVectorProof::startBVConflict(
+    CVC4::BVMinisat::Solver::TLit lit)
+{
+  d_resolutionProof->startResChain(lit);
+}
+
+void ResolutionBitVectorProof::endBVConflict(
+    const CVC4::BVMinisat::Solver::TLitVec& confl)
+{
+  Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict called"
+                  << std::endl;
+
+  std::vector<Expr> expr_confl;
+  for (int i = 0; i < confl.size(); ++i)
+  {
+    prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]);
+    Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr();
+    Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
+    expr_confl.push_back(expr_lit);
+  }
+
+  Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl);
+  Debug("pf::bv") << "Make conflict for " << conflict << std::endl;
+
+  if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end())
+  {
+    Debug("pf::bv") << "Abort...already conflict for " << conflict << std::endl;
+    // This can only happen when we have eager explanations in the bv solver
+    // if we don't get to propagate p before ~p is already asserted
+    d_resolutionProof->cancelResChain();
+    return;
+  }
+
+  // we don't need to check for uniqueness in the sat solver then
+  ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl);
+  d_bbConflictMap[conflict] = clause_id;
+  d_resolutionProof->endResChain(clause_id);
+  Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict id" << clause_id
+                  << " => " << conflict << "\n";
+  d_isAssumptionConflict = false;
+}
+
+void ResolutionBitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts)
+{
+  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  {
+    Debug("pf::bv") << "Construct full proof." << std::endl;
+    d_resolutionProof->constructProof();
+    return;
+  }
+
+  for (unsigned i = 0; i < conflicts.size(); ++i)
+  {
+    Expr confl = conflicts[i];
+    Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl;
+
+    // Special case: if the conflict has a (true) or a (not false) in it, it is
+    // trivial...
+    bool ignoreConflict = false;
+    if ((confl.isConst() && confl.getConst<bool>())
+        || (confl.getKind() == kind::NOT && confl[0].isConst()
+            && !confl[0].getConst<bool>()))
+    {
+      ignoreConflict = true;
+    }
+    else if (confl.getKind() == kind::OR)
+    {
+      for (unsigned k = 0; k < confl.getNumChildren(); ++k)
+      {
+        if ((confl[k].isConst() && confl[k].getConst<bool>())
+            || (confl[k].getKind() == kind::NOT && confl[k][0].isConst()
+                && !confl[k][0].getConst<bool>()))
+        {
+          ignoreConflict = true;
+        }
+      }
+    }
+    if (ignoreConflict)
+    {
+      Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)"
+                      << std::endl;
+      continue;
+    }
+
+    if (d_bbConflictMap.find(confl) != d_bbConflictMap.end())
+    {
+      ClauseId id = d_bbConflictMap[confl];
+      d_resolutionProof->collectClauses(id);
+    }
+    else
+    {
+      // There is no exact match for our conflict, but maybe it is a subset of
+      // another conflict
+      ExprToClauseId::const_iterator it;
+      bool matchFound = false;
+      for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it)
+      {
+        Expr possibleMatch = it->first;
+        if (possibleMatch.getKind() != kind::OR)
+        {
+          // This is a single-node conflict. If this node is in the conflict
+          // we're trying to prove, we have a match.
+          for (unsigned k = 0; k < confl.getNumChildren(); ++k)
+          {
+            if (confl[k] == possibleMatch)
+            {
+              matchFound = true;
+              d_resolutionProof->collectClauses(it->second);
+              break;
+            }
+          }
+        }
+        else
+        {
+          if (possibleMatch.getNumChildren() > confl.getNumChildren()) continue;
+
+          unsigned k = 0;
+          bool matching = true;
+          for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j)
+          {
+            // j is the index in possibleMatch
+            // k is the index in confl
+            while (k < confl.getNumChildren() && confl[k] != possibleMatch[j])
+            {
+              ++k;
+            }
+            if (k == confl.getNumChildren())
+            {
+              // We couldn't find a match for possibleMatch[j], so not a match
+              matching = false;
+              break;
+            }
+          }
+
+          if (matching)
+          {
+            Debug("pf::bv")
+                << "Collecting info from a sub-conflict" << std::endl;
+            d_resolutionProof->collectClauses(it->second);
+            matchFound = true;
+            break;
+          }
+        }
+      }
+
+      if (!matchFound)
+      {
+        Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl
+                        << "Dumping existing conflicts:" << std::endl;
+
+        i = 0;
+        for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it)
+        {
+          ++i;
+          Debug("pf::bv") << "\tConflict #" << i << ": " << it->first
+                          << std::endl;
+        }
+
+        Unreachable();
+      }
+    }
+  }
+}
+
+void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+                                               std::ostream& os,
+                                               std::ostream& paren,
+                                               const ProofLetMap& map)
+{
+  Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called"
+                  << std::endl;
+  Expr conflict = utils::mkSortedExpr(kind::OR, lemma);
+  Debug("pf::bv") << "\tconflict = " << conflict << std::endl;
+
+  if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end())
+  {
+    std::ostringstream lemma_paren;
+    for (unsigned i = 0; i < lemma.size(); ++i)
+    {
+      Expr lit = lemma[i];
+
+      if (lit.getKind() == kind::NOT)
+      {
+        os << "(intro_assump_t _ _ _ ";
+      }
+      else
+      {
+        os << "(intro_assump_f _ _ _ ";
+      }
+      lemma_paren << ")";
+      // print corresponding literal in main sat solver
+      ProofManager* pm = ProofManager::currentPM();
+      CnfProof* cnf = pm->getCnfProof();
+      prop::SatLiteral main_lit = cnf->getLiteral(lit);
+      os << pm->getLitName(main_lit);
+      os << " ";
+      // print corresponding literal in bv sat solver
+      prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
+      os << pm->getAtomName(bb_var, "bb");
+      os << "(\\ unit" << bb_var << "\n";
+      lemma_paren << ")";
+    }
+    Expr lem = utils::mkOr(lemma);
+    Assert(d_bbConflictMap.find(lem) != d_bbConflictMap.end());
+    ClauseId lemma_id = d_bbConflictMap[lem];
+    proof::LFSCProofPrinter::printAssumptionsResolution(
+        d_resolutionProof.get(), lemma_id, os, lemma_paren);
+    os << lemma_paren.str();
+  }
+  else
+  {
+    Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching "
+                       "sub-conflict..."
+                    << std::endl;
+
+    bool matching;
+
+    ExprToClauseId::const_iterator it;
+    unsigned i = 0;
+    for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it)
+    {
+      // Our conflict is sorted, and the records are also sorted.
+      ++i;
+      Expr possibleMatch = it->first;
+
+      if (possibleMatch.getKind() != kind::OR)
+      {
+        // This is a single-node conflict. If this node is in the conflict we're
+        // trying to prove, we have a match.
+        matching = false;
+
+        for (unsigned k = 0; k < conflict.getNumChildren(); ++k)
+        {
+          if (conflict[k] == possibleMatch)
+          {
+            matching = true;
+            break;
+          }
+        }
+      }
+      else
+      {
+        if (possibleMatch.getNumChildren() > conflict.getNumChildren())
+          continue;
+
+        unsigned k = 0;
+
+        matching = true;
+        for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j)
+        {
+          // j is the index in possibleMatch
+          // k is the index in conflict
+          while (k < conflict.getNumChildren()
+                 && conflict[k] != possibleMatch[j])
+          {
+            ++k;
+          }
+          if (k == conflict.getNumChildren())
+          {
+            // We couldn't find a match for possibleMatch[j], so not a match
+            matching = false;
+            break;
+          }
+        }
+      }
+
+      if (matching)
+      {
+        Debug("pf::bv") << "Found a match with conflict #" << i << ": "
+                        << std::endl
+                        << possibleMatch << std::endl;
+        // The rest is just a copy of the usual handling, if a precise match is
+        // found. We only use the literals that appear in the matching conflict,
+        // though, and not in the original lemma - as these may not have even
+        // been bit blasted!
+        std::ostringstream lemma_paren;
+
+        if (possibleMatch.getKind() == kind::OR)
+        {
+          for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i)
+          {
+            Expr lit = possibleMatch[i];
+
+            if (lit.getKind() == kind::NOT)
+            {
+              os << "(intro_assump_t _ _ _ ";
+            }
+            else
+            {
+              os << "(intro_assump_f _ _ _ ";
+            }
+            lemma_paren << ")";
+            // print corresponding literal in main sat solver
+            ProofManager* pm = ProofManager::currentPM();
+            CnfProof* cnf = pm->getCnfProof();
+            prop::SatLiteral main_lit = cnf->getLiteral(lit);
+            os << pm->getLitName(main_lit);
+            os << " ";
+            // print corresponding literal in bv sat solver
+            prop::SatVariable bb_var =
+                d_cnfProof->getLiteral(lit).getSatVariable();
+            os << pm->getAtomName(bb_var, "bb");
+            os << "(\\ unit" << bb_var << "\n";
+            lemma_paren << ")";
+          }
+        }
+        else
+        {
+          // The conflict only consists of one node, either positive or
+          // negative.
+          Expr lit = possibleMatch;
+          if (lit.getKind() == kind::NOT)
+          {
+            os << "(intro_assump_t _ _ _ ";
+          }
+          else
+          {
+            os << "(intro_assump_f _ _ _ ";
+          }
+          lemma_paren << ")";
+          // print corresponding literal in main sat solver
+          ProofManager* pm = ProofManager::currentPM();
+          CnfProof* cnf = pm->getCnfProof();
+          prop::SatLiteral main_lit = cnf->getLiteral(lit);
+          os << pm->getLitName(main_lit);
+          os << " ";
+          // print corresponding literal in bv sat solver
+          prop::SatVariable bb_var =
+              d_cnfProof->getLiteral(lit).getSatVariable();
+          os << pm->getAtomName(bb_var, "bb");
+          os << "(\\ unit" << bb_var << "\n";
+          lemma_paren << ")";
+        }
+
+        ClauseId lemma_id = it->second;
+        proof::LFSCProofPrinter::printAssumptionsResolution(
+            d_resolutionProof.get(), lemma_id, os, lemma_paren);
+        os << lemma_paren.str();
+
+        return;
+      }
+    }
+
+    // We failed to find a matching sub conflict. The last hope is that the
+    // conflict has a FALSE assertion in it; this can happen in some corner
+    // cases, where the FALSE is the result of a rewrite.
+
+    for (unsigned i = 0; i < lemma.size(); ++i)
+    {
+      if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse())
+      {
+        Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl;
+        os << "(clausify_false ";
+        os << ProofManager::getLitName(lemma[i]);
+        os << ")";
+        return;
+      }
+    }
+
+    Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl
+                    << "Dumping existing conflicts:" << std::endl;
+
+    i = 0;
+    for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it)
+    {
+      ++i;
+      Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl;
+    }
+
+    Unreachable();
+  }
+}
+
+void LFSCBitVectorProof::calculateAtomsInBitblastingProof()
+{
+  // Collect the input clauses used
+  IdToSatClause used_lemmas;
+  IdToSatClause used_inputs;
+  d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
+  d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof);
+  Assert(used_lemmas.empty());
+}
+
+void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
+                                              std::ostream& paren,
+                                              ProofLetMap& letMap)
+{
+  // print mapping between theory atoms and internal SAT variables
+  os << std::endl << ";; BB atom mapping\n" << std::endl;
+
+  std::set<Node>::iterator atomIt;
+  Debug("pf::bv") << std::endl
+                  << "BV Dumping atoms from inputs: " << std::endl
+                  << std::endl;
+  for (atomIt = d_atomsInBitblastingProof.begin();
+       atomIt != d_atomsInBitblastingProof.end();
+       ++atomIt)
+  {
+    Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl;
+  }
+  Debug("pf::bv") << std::endl;
+
+  // first print bit-blasting
+  printBitblasting(os, paren);
+
+  // print CNF conversion proof for bit-blasted facts
+  IdToSatClause used_lemmas;
+  IdToSatClause used_inputs;
+  d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
+
+  d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
+  os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl;
+  for (IdToSatClause::iterator it = used_inputs.begin();
+       it != used_inputs.end();
+       ++it)
+  {
+    d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren);
+  }
+
+  os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl;
+  proof::LFSCProofPrinter::printResolutions(d_resolutionProof.get(), os, paren);
+}
+
+} /* namespace proof */
+
+} /* namespace CVC4 */
diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h
new file mode 100644
index 000000000..a54d72d3f
--- /dev/null
+++ b/src/proof/resolution_bitvector_proof.h
@@ -0,0 +1,132 @@
+/*********************                                                        */
+/*! \file resolution_bitvector_proof.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Mathias Preiner, Guy Katz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Bitvector proof
+ **
+ ** Bitvector proof
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
+#define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
+
+#include <iosfwd>
+
+#include "context/context.h"
+#include "expr/expr.h"
+#include "proof/bitvector_proof.h"
+#include "proof/theory_proof.h"
+#include "prop/bvminisat/core/Solver.h"
+
+namespace CVC4 {
+
+namespace theory {
+namespace bv {
+class TheoryBV;
+template <class T>
+class TBitblaster;
+}  // namespace bv
+}  // namespace theory
+
+// TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream
+// header cycle and remove this.
+namespace prop {
+class CnfStream;
+}
+
+} /* namespace CVC4 */
+
+
+namespace CVC4 {
+
+template <class Solver>
+class TSatProof;
+typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof;
+
+namespace proof {
+
+/**
+ * Represents a bitvector proof which is backed by
+ * (a) bitblasting and
+ * (b) a resolution unsat proof.
+ *
+ * Contains tools for constructing BV conflicts
+ */
+class ResolutionBitVectorProof : public BitVectorProof
+{
+ public:
+  ResolutionBitVectorProof(theory::bv::TheoryBV* bv,
+                           TheoryProofEngine* proofEngine);
+
+  /**
+   * Create an (internal) SAT proof object
+   * Must be invoked before manipulating BV conflicts,
+   * or initializing a BNF proof
+   */
+  void initSatProof(CVC4::BVMinisat::Solver* solver);
+
+  BVSatProof* getSatProof();
+
+  /**
+   * Kind of a mess.
+   * In eager mode this must be invoked before printing a proof of the empty
+   * clause. In lazy mode the behavior is ???
+   * TODO(aozdemir) clean this up.
+   */
+  void finalizeConflicts(std::vector<Expr>& conflicts);
+
+  void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
+  void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
+  void endBVConflict(const BVMinisat::Solver::TLitVec& confl);
+
+  void markAssumptionConflict() { d_isAssumptionConflict = true; }
+  bool isAssumptionConflict() const { return d_isAssumptionConflict; }
+
+  virtual void printResolutionProof(std::ostream& os,
+                                    std::ostream& paren,
+                                    ProofLetMap& letMap) = 0;
+
+  void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override;
+
+ protected:
+  // The CNF formula that results from bit-blasting will need a proof.
+  // This is that proof.
+  std::unique_ptr<BVSatProof> d_resolutionProof;
+
+  bool d_isAssumptionConflict;
+
+  theory::TheoryId getTheoryId() override;
+  context::Context d_fakeContext;
+};
+
+class LFSCBitVectorProof : public ResolutionBitVectorProof
+{
+ public:
+  LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+      : ResolutionBitVectorProof(bv, proofEngine)
+  {
+  }
+  void printTheoryLemmaProof(std::vector<Expr>& lemma,
+                             std::ostream& os,
+                             std::ostream& paren,
+                             const ProofLetMap& map) override;
+  void printResolutionProof(std::ostream& os,
+                            std::ostream& paren,
+                            ProofLetMap& letMap) override;
+  void calculateAtomsInBitblastingProof() override;
+};
+
+}  // namespace proof
+
+}  // namespace CVC4
+
+#endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index cfad0a068..ee06fbfa0 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -22,12 +22,12 @@
 #include "options/proof_options.h"
 #include "proof/arith_proof.h"
 #include "proof/array_proof.h"
-#include "proof/bitvector_proof.h"
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/proof_output_channel.h"
 #include "proof/proof_utils.h"
+#include "proof/resolution_bitvector_proof.h"
 #include "proof/sat_proof.h"
 #include "proof/simplify_boolean_node.h"
 #include "proof/uf_proof.h"
@@ -46,6 +46,9 @@
 
 namespace CVC4 {
 
+using proof::LFSCBitVectorProof;
+using proof::ResolutionBitVectorProof;
+
 unsigned CVC4::ProofLetCount::counter = 0;
 static unsigned LET_COUNT = 1;
 
@@ -77,7 +80,8 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
       }
 
       if (id == theory::THEORY_BV) {
-        BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this);
+        auto bv_theory = static_cast<theory::bv::TheoryBV*>(th);
+        ResolutionBitVectorProof* bvp = new LFSCBitVectorProof(bv_theory, this);
         d_theoryProofTable[id] = bvp;
         return;
       }
@@ -102,9 +106,9 @@ void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) {
     theory::TheoryId id = th->getId();
     if (id == theory::THEORY_BV) {
       Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end());
-
-      BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id];
-      ((theory::bv::TheoryBV*)th)->setProofLog( bvp );
+      ResolutionBitVectorProof* bvp =
+          (ResolutionBitVectorProof*)d_theoryProofTable[id];
+      ((theory::bv::TheoryBV*)th)->setResolutionProofLog(bvp);
       return;
     }
   }
@@ -529,7 +533,7 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std
     }
   }
 
-  BitVectorProof* bv = ProofManager::getBitVectorProof();
+  ResolutionBitVectorProof* bv = ProofManager::getBitVectorProof();
   bv->finalizeConflicts(bv_lemmas);
   //  bv->printResolutionProof(os, paren, letMap);
 }