diff options
Diffstat (limited to 'src/proof/array_proof.h')
-rw-r--r-- | src/proof/array_proof.h | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 372ad1f67..9660fbe50 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -82,7 +82,9 @@ protected: theory::TheoryId getTheoryId() override; public: - ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine); + ArrayProof(Environment* env, + theory::arrays::TheoryArrays* arrays, + TheoryProofEngine* proofEngine); std::string skolemToLiteral(Expr skolem); @@ -91,9 +93,12 @@ protected: class LFSCArrayProof : public ArrayProof { public: - LFSCArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine) - : ArrayProof(arrays, proofEngine) - {} + LFSCArrayProof(Environment* env, + theory::arrays::TheoryArrays* arrays, + TheoryProofEngine* proofEngine) + : ArrayProof(env, arrays, proofEngine) + { + } void printOwnedTerm(Expr term, std::ostream& os, |