Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. (#1374)
authorTim King <taking@cs.nyu.edu>
Thu, 16 Nov 2017 02:17:56 +0000 (18:17 -0800)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 16 Nov 2017 02:17:56 +0000 (20:17 -0600)
src/proof/bitvector_proof.cpp

index 5c660b284871c4a5ab2622dce0f96ffcb91b71a2..907c809ddb6b249305a6568224b5f35321da0417 100644 (file)
@@ -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);