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