Enable CryptoMiniSat-backed BV proofs (#2847)

* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
   * Specifically, CNF proofs broke when proving tautological clauses.
     Now they don't.

14 files changed, 328 insertions, 81 deletions

diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index f154e5c90..79b0bff9c 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -250,6 +250,8 @@ bool Configuration::isBuiltWithCryptominisat() {
   return IS_CRYPTOMINISAT_BUILD;
 }
 
+bool Configuration::isBuiltWithDrat2Er() { return IS_DRAT2ER_BUILD; }
+
 bool Configuration::isBuiltWithReadline() {
   return IS_READLINE_BUILD;
 }
diff --git a/src/base/configuration.h b/src/base/configuration.h
index b6e2a1963..7900e877e 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -97,6 +97,8 @@ public:
 
   static bool isBuiltWithCryptominisat();
 
+  static bool isBuiltWithDrat2Er();
+
   static bool isBuiltWithReadline();
 
   static bool isBuiltWithLfsc();
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index c4541f4e4..6dd755625 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -7,7 +7,7 @@ header = "options/bv_options.h"
   category   = "expert"
   long       = "bv-proof-format=MODE"
   type       = "CVC4::theory::bv::BvProofFormat"
-  default    = "CVC4::theory::bv::BITVECTOR_PROOF_LRAT"
+  default    = "CVC4::theory::bv::BITVECTOR_PROOF_ER"
   handler    = "stringToBvProofFormat"
   predicates = ["satSolverEnabledBuild"]
   includes   = ["options/bv_bitblast_mode.h"]
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 84b9f3b4c..ad4fc8d48 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1769,10 +1769,11 @@ void OptionsHandler::proofEnabledBuild(std::string option, bool value)
 {
 #ifdef CVC4_PROOF
   if (value && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
-      && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT)
+      && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT
+      && options::bvSatSolver() != theory::bv::SAT_SOLVER_CRYPTOMINISAT)
   {
     throw OptionException(
-        "Eager BV proofs only supported when minisat is used");
+        "Eager BV proofs only supported when MiniSat or CryptoMiniSat is used");
   }
 #else
   if(value) {
@@ -1938,6 +1939,7 @@ void OptionsHandler::showConfiguration(std::string option) {
   print_config_cond("glpk", Configuration::isBuiltWithGlpk());
   print_config_cond("cadical", Configuration::isBuiltWithCadical());
   print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
+  print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er());
   print_config_cond("gmp", Configuration::isBuiltWithGmp());
   print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
   print_config_cond("readline", Configuration::isBuiltWithReadline());
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 90c0c9b30..b42a464ab 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -221,6 +221,14 @@ void BitVectorProof::printOwnedTerm(Expr term,
   }
 }
 
+void BitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                           std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+}
+
 void BitVectorProof::printBitOf(Expr term,
                                 std::ostream& os,
                                 const ProofLetMap& map)
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 4b897a6c6..d963f6d61 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -167,7 +167,7 @@ class BitVectorProof : public TheoryProof
    * @param os the stream to print to
    * @param paren any parentheses to add to the end of the global proof
    */
-  virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren) = 0;
+  virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren);
 
   /**
    * Read the d_atomsInBitblastingProof member.
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index bb875d1d8..eed295b1a 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -19,10 +19,13 @@
 #include <algorithm>
 #include <iterator>
 #include <set>
+
 #include "options/bv_options.h"
 #include "proof/clausal_bitvector_proof.h"
 #include "proof/drat/drat_proof.h"
+#include "proof/er/er_proof.h"
 #include "proof/lfsc_proof_printer.h"
+#include "proof/lrat/lrat_proof.h"
 #include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
@@ -66,12 +69,12 @@ void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
 void ClausalBitVectorProof::registerUsedClause(ClauseId id,
                                                prop::SatClause& clause)
 {
-  d_usedClauses.emplace_back(
-      id, std::unique_ptr<prop::SatClause>(new prop::SatClause(clause)));
+  d_usedClauses.emplace_back(id, clause);
 };
 
 void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
 {
+  // Debug dump of DRAT Proof
   if (Debug.isOn("bv::clausal"))
   {
     std::string serializedDratProof = d_binaryDratProof.str();
@@ -84,7 +87,16 @@ void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
     Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
     dratProof.outputAsText(Debug("bv::clausal"));
   }
-  Unimplemented();
+
+  // Empty any old record of which atoms were used
+  d_atomsInBitblastingProof.clear();
+
+  // For each used clause, ask the CNF proof which atoms are used in it
+  for (const auto& usedIndexAndClause : d_usedClauses)
+  {
+    d_cnfProof->collectAtoms(&usedIndexAndClause.second,
+                             d_atomsInBitblastingProof);
+  }
 }
 
 void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
@@ -101,13 +113,91 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
                                                          std::ostream& paren,
                                                          ProofLetMap& letMap)
 {
-  Unimplemented();
+  os << "\n;; Bitblasting mappings\n";
+  printBitblasting(os, paren);
+
+  os << "\n;; BB-CNF mappings\n";
+  d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
+
+  os << "\n;; BB-CNF proofs\n";
+  for (const auto& idAndClause : d_usedClauses)
+  {
+    d_cnfProof->printCnfProofForClause(
+        idAndClause.first, &idAndClause.second, os, paren);
+  }
 }
 
-void LfscClausalBitVectorProof::printEmptyClauseProof(std::ostream& os,
-                                                      std::ostream& paren)
+void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                   std::ostream& paren)
 {
-  Unimplemented();
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+
+  os << "\n;; Proof of input to SAT solver\n";
+  os << "(@ proofOfSatInput ";
+  paren << ")";
+  std::vector<ClauseId> usedIds;
+  usedIds.reserve(d_usedClauses.size());
+  for (const auto& idAnd : d_usedClauses)
+  {
+    usedIds.push_back(idAnd.first);
+  };
+  LFSCProofPrinter::printSatInputProof(usedIds, os, "bb");
+
+  os << "\n;; DRAT Proof Value\n";
+  os << "(@ dratProof ";
+  paren << ")";
+  drat::DratProof::fromBinary(d_binaryDratProof.str()).outputAsLfsc(os, 2);
+  os << "\n";
+
+  os << "\n;; Verification of DRAT Proof\n";
+  os << "(drat_proof_of_bottom _ proofOfSatInput dratProof "
+     << "\n)";
+}
+
+void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                   std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+
+  os << "\n;; Proof of input to SAT solver\n";
+  os << "(@ proofOfCMap ";
+  paren << ")";
+  std::vector<ClauseId> usedIds;
+  usedIds.reserve(d_usedClauses.size());
+  for (const auto& idAnd : d_usedClauses)
+  {
+    usedIds.push_back(idAnd.first);
+  };
+  LFSCProofPrinter::printCMapProof(usedIds, os, "bb");
+
+  os << "\n;; DRAT Proof Value\n";
+  os << "(@ lratProof ";
+  paren << ")";
+  lrat::LratProof pf =
+      lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str());
+  pf.outputAsLfsc(os);
+  os << "\n";
+
+  os << "\n;; Verification of DRAT Proof\n";
+  os << "(lrat_proof_of_bottom _ proofOfCMap lratProof "
+     << "\n)";
+}
+
+void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                 std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+
+  er::ErProof pf =
+      er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str());
+
+  pf.outputAsLfsc(os);
 }
 
 }  // namespace proof
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
index 85e409e0d..cd215da36 100644
--- a/src/proof/clausal_bitvector_proof.h
+++ b/src/proof/clausal_bitvector_proof.h
@@ -61,8 +61,7 @@ class ClausalBitVectorProof : public BitVectorProof
 
  protected:
   // A list of all clauses and their ids which are passed into the SAT solver
-  std::vector<std::pair<ClauseId, std::unique_ptr<prop::SatClause>>>
-      d_usedClauses;
+  std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
   // Stores the proof recieved from the SAT solver.
   std::ostringstream d_binaryDratProof;
 };
@@ -77,7 +76,6 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof
                             TheoryProofEngine* proofEngine)
       : ClausalBitVectorProof(bv, proofEngine)
   {
-    // That's all!
   }
 
   void printTheoryLemmaProof(std::vector<Expr>& lemma,
@@ -87,6 +85,49 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof
   void printBBDeclarationAndCnf(std::ostream& os,
                                 std::ostream& paren,
                                 ProofLetMap& letMap) override;
+};
+
+/**
+ * A DRAT proof for a bit-vector problem
+ */
+class LfscDratBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+  LfscDratBitVectorProof(theory::bv::TheoryBV* bv,
+                         TheoryProofEngine* proofEngine)
+      : LfscClausalBitVectorProof(bv, proofEngine)
+  {
+  }
+
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+/**
+ * An LRAT proof for a bit-vector problem
+ */
+class LfscLratBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+  LfscLratBitVectorProof(theory::bv::TheoryBV* bv,
+                         TheoryProofEngine* proofEngine)
+      : LfscClausalBitVectorProof(bv, proofEngine)
+  {
+  }
+
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+/**
+ * An Extended Resolution proof for a bit-vector problem
+ */
+class LfscErBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+  LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+      : LfscClausalBitVectorProof(bv, proofEngine)
+  {
+  }
+
   void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
 };
 
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 4e8d20162..aed889e33 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -349,6 +349,39 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
   }
 }
 
+// Detects whether a clause has x v ~x for some x
+// If so, returns the positive occurence's idx first, then the negative's
+Maybe<std::pair<size_t, size_t>> CnfProof::detectTrivialTautology(
+    const prop::SatClause& clause)
+{
+  // a map from a SatVariable to its previous occurence's polarity and location
+  std::map<prop::SatVariable, std::pair<bool, size_t>> varsToPolsAndIndices;
+  for (size_t i = 0; i < clause.size(); ++i)
+  {
+    prop::SatLiteral lit = clause[i];
+    prop::SatVariable var = lit.getSatVariable();
+    bool polarity = !lit.isNegated();
+
+    // Check if this var has already occured w/ opposite polarity
+    auto iter = varsToPolsAndIndices.find(var);
+    if (iter != varsToPolsAndIndices.end() && iter->second.first != polarity)
+    {
+      if (iter->second.first)
+      {
+        return Maybe<std::pair<size_t, size_t>>{
+            std::make_pair(iter->second.second, i)};
+      }
+      else
+      {
+        return Maybe<std::pair<size_t, size_t>>{
+            std::make_pair(i, iter->second.second)};
+      }
+    }
+    varsToPolsAndIndices[var] = std::make_pair(polarity, i);
+  }
+  return Maybe<std::pair<size_t, size_t>>{};
+}
+
 void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
                                     std::ostream& os,
                                     std::ostream& paren) {
@@ -431,61 +464,98 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
 
   Assert( clause->size()>0 );
 
-  Node base_assertion = getDefinitionForClause(id);
-
-  //get the assertion for the clause id
-  std::map<Node, unsigned > childIndex;
-  std::map<Node, bool > childPol;
-  Node assertion = clauseToNode( *clause, childIndex, childPol );
-  //if there is no reason, construct assertion directly.   This can happen for unit clauses.
-  if( base_assertion.isNull() ){
-    base_assertion = assertion;
+  // If the clause contains x v ~x, it's easy!
+  //
+  // It's important to check for this case, because our other logic for
+  // recording the location of variables in the clause assumes the clause is
+  // not tautological
+  Maybe<std::pair<size_t, size_t>> isTrivialTaut =
+      detectTrivialTautology(*clause);
+  if (isTrivialTaut.just())
+  {
+    size_t posIndexInClause = isTrivialTaut.value().first;
+    size_t negIndexInClause = isTrivialTaut.value().second;
+    Trace("cnf-pf") << "; Indices " << posIndexInClause << " (+) and "
+                    << negIndexInClause << " (-) make this clause a tautology"
+                    << std::endl;
+
+    std::string proofOfPos =
+        ProofManager::getLitName((*clause)[negIndexInClause], d_name);
+    std::string proofOfNeg =
+        ProofManager::getLitName((*clause)[posIndexInClause], d_name);
+    os << "(contra _ " << proofOfPos << " " << proofOfNeg << ")";
   }
-  //os_base is proof of base_assertion
-  std::stringstream os_base;
-
-  // checks if tautological definitional clause or top-level clause
-  // and prints the proof of the top-level formula
-  bool is_input = printProofTopLevel(base_assertion, os_base);
+  else
+  {
+    Node base_assertion = getDefinitionForClause(id);
+
+    // get the assertion for the clause id
+    std::map<Node, unsigned> childIndex;
+    std::map<Node, bool> childPol;
+    Node assertion = clauseToNode(*clause, childIndex, childPol);
+    // if there is no reason, construct assertion directly.   This can happen
+    // for unit clauses.
+    if (base_assertion.isNull())
+    {
+      base_assertion = assertion;
+    }
+    // os_base is proof of base_assertion
+    std::stringstream os_base;
+
+    // checks if tautological definitional clause or top-level clause
+    // and prints the proof of the top-level formula
+    bool is_input = printProofTopLevel(base_assertion, os_base);
+
+    if (is_input)
+    {
+      Debug("cnf-pf") << std::endl
+                      << "; base assertion is input. proof: " << os_base.str()
+                      << std::endl;
+    }
 
-  if (is_input) {
-    Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl;
-  }
+    // get base assertion with polarity
+    bool base_pol = base_assertion.getKind() != kind::NOT;
+    base_assertion = base_assertion.getKind() == kind::NOT ? base_assertion[0]
+                                                           : base_assertion;
 
-  //get base assertion with polarity
-  bool base_pol = base_assertion.getKind()!=kind::NOT;
-  base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion;
-
-  std::map< Node, unsigned >::iterator itci = childIndex.find( base_assertion );
-  bool is_in_clause = itci!=childIndex.end();
-  unsigned base_index = is_in_clause ? itci->second : 0;
-  Trace("cnf-pf") << std::endl;
-  Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl;
-  if (!is_input){
-    Assert(is_in_clause);
-    prop::SatLiteral blit = (*clause)[ base_index ];
-    os_base << ProofManager::getLitName(blit, d_name);
-    base_pol = !childPol[base_assertion]; // WHY? if the case is =>
-  }
-  Trace("cnf-pf") << "; polarity of base assertion = " << base_pol << std::endl;
-  Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl;
-
-  bool success = false;
-  if( is_input &&
-      is_in_clause &&
-      childPol[base_assertion]==base_pol ){
-    //if both in input and in clause, the proof is trivial.  this is the case for unit clauses.
-    Trace("cnf-pf") << "; trivial" << std::endl;
-    os << "(contra _ ";
-    success = true;
-    prop::SatLiteral lit = (*clause)[itci->second];
-    if( base_pol ){
-      os << os_base.str() << " " << ProofManager::getLitName(lit, d_name);
-    }else{
-      os << ProofManager::getLitName(lit, d_name) << " " << os_base.str();
+    std::map<Node, unsigned>::iterator itci = childIndex.find(base_assertion);
+    bool is_in_clause = itci != childIndex.end();
+    unsigned base_index = is_in_clause ? itci->second : 0;
+    Trace("cnf-pf") << std::endl;
+    Trace("cnf-pf") << "; input = " << is_input
+                    << ", is_in_clause = " << is_in_clause << ", id = " << id
+                    << ", assertion = " << assertion
+                    << ", base assertion = " << base_assertion << std::endl;
+    if (!is_input)
+    {
+      Assert(is_in_clause);
+      prop::SatLiteral blit = (*clause)[base_index];
+      os_base << ProofManager::getLitName(blit, d_name);
+      base_pol = !childPol[base_assertion];  // WHY? if the case is =>
     }
-    os << ")";
-  } else if ((base_assertion.getKind()==kind::AND && !base_pol) ||
+    Trace("cnf-pf") << "; polarity of base assertion = " << base_pol
+                    << std::endl;
+    Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl;
+
+    bool success = false;
+    if (is_input && is_in_clause && childPol[base_assertion] == base_pol)
+    {
+      // if both in input and in clause, the proof is trivial.  this is the case
+      // for unit clauses.
+      Trace("cnf-pf") << "; trivial" << std::endl;
+      os << "(contra _ ";
+      success = true;
+      prop::SatLiteral lit = (*clause)[itci->second];
+      if (base_pol)
+      {
+        os << os_base.str() << " " << ProofManager::getLitName(lit, d_name);
+      }
+      else
+      {
+        os << ProofManager::getLitName(lit, d_name) << " " << os_base.str();
+      }
+      os << ")";
+    } else if ((base_assertion.getKind()==kind::AND && !base_pol) ||
            ((base_assertion.getKind()==kind::OR ||
              base_assertion.getKind()==kind::IMPLIES) && base_pol)) {
     Trace("cnf-pf") << "; and/or case 1" << std::endl;
@@ -776,6 +846,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
     Trace("cnf-pf") << std::endl;
     os << "trust-bad";
   }
+  }
 
   os << ")" << clause_paren.str()
      << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 78ddeebd0..481e77c75 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -29,6 +29,7 @@
 #include "proof/clause_id.h"
 #include "proof/lemma_proof.h"
 #include "proof/sat_proof.h"
+#include "util/maybe.h"
 #include "util/proof.h"
 
 namespace CVC4 {
@@ -164,6 +165,10 @@ public:
                            std::ostream& paren,
                            ProofLetMap &letMap) = 0;
 
+  // Detects whether a clause has x v ~x for some x
+  // If so, returns the positive occurence's idx first, then the negative's
+  static Maybe<std::pair<size_t, size_t>> detectTrivialTautology(
+      const prop::SatClause& clause);
   virtual void printClause(const prop::SatClause& clause,
                            std::ostream& os,
                            std::ostream& paren) = 0;
diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp
index c2f2fa49e..5b9487a00 100644
--- a/src/proof/drat/drat_proof.cpp
+++ b/src/proof/drat/drat_proof.cpp
@@ -259,12 +259,12 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const
     {
       case ADDITION:
       {
-        os << "DRATProofa";
+        os << "DRATProofa ";
         break;
       }
       case DELETION:
       {
-        os << "DRATProofd";
+        os << "DRATProofd ";
         break;
       }
       default: { Unreachable("Unrecognized DRAT instruction kind");
@@ -273,7 +273,7 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const
     for (const SatLiteral& l : i.d_clause)
     {
       os << "(clc (" << (l.isNegated() ? "neg " : "pos ")
-         << ProofManager::getVarName(l.getSatVariable()) << ") ";
+         << ProofManager::getVarName(l.getSatVariable(), "bb") << ") ";
     }
     os << "cln";
     std::fill_n(std::ostream_iterator<char>(os), i.d_clause.size(), ')');
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 452b64b11..22903c3c9 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -102,12 +102,12 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
   // Write the formula
   std::ofstream formStream(formulaFilename);
   printDimacs(formStream, usedClauses);
-  unlink(formulaFilename);
+  formStream.close();
 
   // Write the (binary) DRAT proof
   std::ofstream dratStream(dratFilename);
   dratStream << dratBinary;
-  unlink(dratFilename);
+  dratStream.close();
 
   // Invoke drat2er
 #if CVC4_USE_DRAT2ER
@@ -115,7 +115,8 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
                                              dratFilename,
                                              tracecheckFilename,
                                              false,
-                                             drat2er::options::QUIET);
+                                             drat2er::options::QUIET,
+                                             false);
 
 #else
   Unimplemented(
@@ -126,13 +127,11 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
   // Parse the resulting TRACECHECK proof into an ER proof.
   std::ifstream tracecheckStream(tracecheckFilename);
   ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream));
-  unlink(tracecheckFilename);
-
-  formStream.close();
-  dratStream.close();
   tracecheckStream.close();
 
-
+  remove(formulaFilename);
+  remove(dratFilename);
+  remove(tracecheckFilename);
 
   return proof;
 }
@@ -156,6 +155,15 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
     {
       Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
       Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
+      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+          traceCheckClause{d_tracecheck.d_lines[i].d_clause.begin(),
+                           d_tracecheck.d_lines[i].d_clause.end()};
+      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+          originalClause{usedClauses[i].second.begin(),
+                         usedClauses[i].second.end()};
+      Assert(traceCheckClause == originalClause);
+      Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
+      Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
       Assert(d_tracecheck.d_lines[i].d_clause.size()
              == usedClauses[i].second.size());
       for (size_t j = 0, m = usedClauses[i].second.size(); j < m; ++j)
@@ -185,7 +193,7 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
     // Look at the negation of the second literal in the second clause to get
     // the old literal
     AlwaysAssert(d_tracecheck.d_lines.size() > i + 1,
-        "Malformed definition in TRACECHECK proof from drat2er");
+                 "Malformed definition in TRACECHECK proof from drat2er");
     d_definitions.emplace_back(newVar,
                                ~d_tracecheck.d_lines[i + 1].d_clause[1],
                                std::move(otherLiterals));
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 5f0ade86a..ace41892f 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -734,8 +734,7 @@ void LFSCProof::toStream(std::ostream& out) const
 
   out << ";; Printing final unsat proof \n";
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
-    proof::LFSCProofPrinter::printResolutionEmptyClause(
-        ProofManager::getBitVectorProof()->getSatProof(), out, paren);
+    ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren);
   } else {
     // print actual resolution proof
     proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index fe9acfef3..66805ecd4 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -85,8 +85,27 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
         if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
             && options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT)
         {
-          proof::BitVectorProof* bvp =
-              new proof::LfscClausalBitVectorProof(thBv, this);
+          proof::BitVectorProof* bvp = nullptr;
+          switch (options::bvProofFormat())
+          {
+            case theory::bv::BvProofFormat::BITVECTOR_PROOF_DRAT:
+            {
+              bvp = new proof::LfscDratBitVectorProof(thBv, this);
+              break;
+            }
+            case theory::bv::BvProofFormat::BITVECTOR_PROOF_LRAT:
+            {
+              bvp = new proof::LfscLratBitVectorProof(thBv, this);
+              break;
+            }
+            case theory::bv::BvProofFormat::BITVECTOR_PROOF_ER:
+            {
+              bvp = new proof::LfscErBitVectorProof(thBv, this);
+              break;
+            }
+            default: { Unreachable("Invalid BvProofFormat");
+            }
+          };
           d_theoryProofTable[id] = bvp;
         }
         else