1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 019918c2f..1e557bb64 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -32,11 +32,8 @@ namespace bv {
 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
     : TBitblaster<Node>(),
       d_context(c),
-      d_nullContext(new context::Context()),
       d_satSolver(),
       d_bitblastingRegistrar(new BitblastingRegistrar(this)),
-      d_cnfStream(),
-      d_bvp(nullptr),
       d_bv(theory_bv),
       d_bbAtoms(),
       d_variables(),
@@ -268,13 +265,6 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
   return true;
 }
 
-void EagerBitblaster::setResolutionProofLog(
-    proof::ResolutionBitVectorProof* bvp)
-{
-  THEORY_PROOF(d_bvp = bvp; d_satSolver->setProofLog(bvp);
-               bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());)
-}
-
 bool EagerBitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }