diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-15 18:17:56 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-15 20:17:56 -0600 |
commit | 7bd874b098f210b53f5b608bc159d1d90c8794b8 (patch) | |
tree | cdb22726afd8d092b696825d4d026f123b7f3d20 /src/proof/bitvector_proof.cpp | |
parent | 9bff14c12c34fea0e6ba0649a3e8f7e8f48b5646 (diff) |
Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. (#1374)
Diffstat (limited to 'src/proof/bitvector_proof.cpp')
-rw-r--r-- | src/proof/bitvector_proof.cpp | 23 |
1 files 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); |