Fix missing-override warning (#2811)

`TLazyBitblaster::setProofLog()` was defined even though the method was
not virtual before PR #2808 and `TBitblaster` was implementing the same
method. After that PR, which made the method virtual, GCC complained
about a missing `override` keyword for `setProofLog()`. However, the
method should have been removed (see
[comment](https://github.com/CVC4/CVC4/pull/2786#discussion_r247299617)).
This commit removes the function definition.

diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 2a47c231577054d855fa09779fa569facf4aeb3d..3b44bfddfba330a8d2c8ec857c4b96d2ca624ada 100644 (file)
--- 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 9af74d8dbddfa2dd5819ae3a23a6d16ac20d6813..8dbf7807db3915afe5158aea20adefd7dfc342b1 100644 (file)
--- 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(); }