From b4c9b783384fb05a3e71ff535b5f790e79c28a94 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 19 Jan 2019 03:34:43 -0800 Subject: [PATCH] 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. --- src/theory/bv/bitblast/lazy_bitblaster.cpp | 8 -------- src/theory/bv/bitblast/lazy_bitblaster.h | 1 - 2 files changed, 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 * 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(); } -- 2.30.2