Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR

1 files changed, 1 insertions, 11 deletions

diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 36aa72da3..d1490374d 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -33,8 +33,7 @@ EagerBitblastSolver::EagerBitblastSolver(context::Context* c, TheoryBV* bv)
       d_bitblaster(),
       d_aigBitblaster(),
       d_useAig(options::bitvectorAig()),
-      d_bv(bv),
-      d_bvp(nullptr)
+      d_bv(bv)
 {
 }
 
@@ -55,10 +54,6 @@ void EagerBitblastSolver::initialize() {
 #endif
   } else {
     d_bitblaster.reset(new EagerBitblaster(d_bv, d_context));
-    THEORY_PROOF(if (d_bvp) {
-      d_bitblaster->setProofLog(d_bvp);
-      d_bvp->setBitblaster(d_bitblaster.get());
-    });
   }
 }
 
@@ -127,11 +122,6 @@ bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
   return d_bitblaster->collectModelInfo(m, fullModel);
 }
 
-void EagerBitblastSolver::setProofLog(proof::BitVectorProof* bvp)
-{
-  d_bvp = bvp;
-}
-
 }  // namespace bv
 }  // namespace theory
 }  // namespace CVC4