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