From: Tim King <taking@cs.nyu.edu>
Date: Thu, 16 Nov 2017 02:17:56 +0000 (-0800)
Subject: Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. (#1374)
X-Git-Tag: cvc5-1.0.0~5469
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7bd874b098f210b53f5b608bc159d1d90c8794b8;p=cvc5.git

Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. (#1374)
---

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