summaryrefslogtreecommitdiff
path: root/src/proof/uf_proof.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/uf_proof.h')
-rw-r--r--src/proof/uf_proof.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 7aa00cc35..a4e4cff0b 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -62,8 +62,9 @@ class UFProof : public TheoryProof {
protected:
TypeSet d_sorts; // all the uninterpreted sorts in this theory
ExprSet d_declarations; // all the variable/function declarations
+ theory::TheoryId getTheoryId();
-public:
+ public:
UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine);
void registerTerm(Expr term) override;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback