From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sat, 19 Jan 2019 11:34:43 +0000 (-0800)
Subject: Fix missing-override warning (#2811)
X-Git-Tag: cvc5-1.0.0~4276
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b4c9b783384fb05a3e71ff535b5f790e79c28a94;p=cvc5.git

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 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(); }