From 7bd874b098f210b53f5b608bc159d1d90c8794b8 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 15 Nov 2017 18:17:56 -0800 Subject: [PATCH] Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. (#1374) --- src/proof/bitvector_proof.cpp | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 5c660b284..907c809dd 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -33,17 +33,18 @@ using namespace CVC4::theory::bv; namespace CVC4 { -BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : TheoryProof(bv, proofEngine) - , d_declarations() - , d_seenBBTerms() - , d_bbTerms() - , d_bbAtoms() - , d_resolutionProof(NULL) - , d_cnfProof(NULL) - , d_bitblaster(NULL) - , d_useConstantLetification(false) -{} +BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) + : TheoryProof(bv, proofEngine), + d_declarations(), + d_seenBBTerms(), + d_bbTerms(), + d_bbAtoms(), + d_resolutionProof(NULL), + d_cnfProof(NULL), + d_isAssumptionConflict(false), + d_bitblaster(NULL), + d_useConstantLetification(false) {} void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) { Assert (d_resolutionProof == NULL); -- 2.30.2