diff options
Diffstat (limited to 'src/proof/resolution_bitvector_proof.h')
| -rw-r--r-- | src/proof/resolution_bitvector_proof.h | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h index 5fd11092f..eac469ff7 100644 --- a/src/proof/resolution_bitvector_proof.h +++ b/src/proof/resolution_bitvector_proof.h @@ -48,7 +48,8 @@ namespace proof { class ResolutionBitVectorProof : public BitVectorProof { public: - ResolutionBitVectorProof(theory::bv::TheoryBV* bv, + ResolutionBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); /** @@ -90,9 +91,10 @@ class ResolutionBitVectorProof : public BitVectorProof class LfscResolutionBitVectorProof : public ResolutionBitVectorProof { public: - LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv, + LfscResolutionBitVectorProof(Environment* env, + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : ResolutionBitVectorProof(bv, proofEngine) + : ResolutionBitVectorProof(env, bv, proofEngine) { } void printTheoryLemmaProof(std::vector<Expr>& lemma, |