[SMTChecker] Implement uninterpreted functions and use it for blockhash()

1 files changed, 2 insertions, 1 deletions

diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index eb876a7f..08ad74da 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -49,7 +49,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
 	void declareInteger(std::string _name) override;
 	void declareBool(std::string _name) override;
 
@@ -58,6 +58,7 @@ public:
 
 private:
 	std::string toSExpr(Expression const& _expr);
+	std::string toSmtLibSort(Sort _sort);
 
 	void write(std::string _data);