2 files changed, 0 insertions, 9 deletions
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 2a47c2315..3b44bfddf 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -564,14 +564,6 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
   return true;
 }
 
-void TLazyBitblaster::setProofLog(proof::BitVectorProof* bvp)
-{
-  THEORY_PROOF(d_bvp = bvp; bvp->attachToSatSolver(*d_satSolver);
-               prop::SatVariable t = d_satSolver->trueVar();
-               prop::SatVariable f = d_satSolver->falseVar();
-               bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f));
-}
-
 void TLazyBitblaster::clearSolver() {
   Assert (d_ctx->getLevel() == 0);
   d_assertedAtoms->deleteSelf();
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 9af74d8db..8dbf7807d 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -77,7 +77,6 @@ class TLazyBitblaster : public TBitblaster<Node>
    * constants to equivalence classes that don't already have them
    */
   bool collectModelInfo(TheoryModel* m, bool fullModel);
-  void setProofLog(proof::BitVectorProof* bvp);
 
   typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }