1 files changed, 7 insertions, 7 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index ba3533cc3..90c0c9b30 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -18,10 +18,13 @@
 #include "options/proof_options.h"
 #include "proof/proof_output_channel.h"
 #include "proof/theory_proof.h"
+#include "prop/sat_solver_types.h"
 #include "theory/bv/bitblast/bitblaster.h"
 #include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
+
+namespace proof {
 BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv,
                                TheoryProofEngine* proofEngine)
     : TheoryProof(bv, proofEngine),
@@ -118,13 +121,6 @@ std::string BitVectorProof::getBBTermName(Expr expr)
   return os.str();
 }
 
-void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
-                                  context::Context* cnf)
-{
-  Assert(d_cnfProof == nullptr);
-  d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb"));
-}
-
 void BitVectorProof::printOwnedTerm(Expr term,
                                     std::ostream& os,
                                     const ProofLetMap& map)
@@ -709,6 +705,8 @@ void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
   }
 }
 
+theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; }
+
 const std::set<Node>* BitVectorProof::getAtomsInBitblastingProof()
 {
   return &d_atomsInBitblastingProof;
@@ -774,4 +772,6 @@ void BitVectorProof::printRewriteProof(std::ostream& os,
   os << ")";
 }
 
+}  // namespace proof
+
 }  // namespace CVC4