1 files changed, 14 insertions, 13 deletions
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index af1cc8e4..a6618fb5 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -45,9 +45,7 @@ enum class CheckResult
 enum class Sort
 {
 	Int,
-	Bool,
-	IntIntFun, // Function of one Int returning a single Int
-	IntBoolFun // Function of one Int returning a single Bool
+	Bool
 };
 
 /// C++ representation of an SMTLIB2 expression.
@@ -150,7 +148,7 @@ public:
 	{
 		return Expression("/", std::move(_a), std::move(_b), Sort::Int);
 	}
-	Expression operator()(Expression _a) const
+	Expression operator()(std::vector<Expression> _arguments) const
 	{
 		solAssert(
 			arguments.empty(),
@@ -158,10 +156,10 @@ public:
 		);
 		switch (sort)
 		{
-		case Sort::IntIntFun:
-			return Expression(name, _a, Sort::Int);
-		case Sort::IntBoolFun:
-			return Expression(name, _a, Sort::Bool);
+		case Sort::Int:
+			return Expression(name, std::move(_arguments), Sort::Int);
+		case Sort::Bool:
+			return Expression(name, std::move(_arguments), Sort::Bool);
 		default:
 			solAssert(
 				false,
@@ -199,18 +197,21 @@ public:
 	virtual void push() = 0;
 	virtual void pop() = 0;
 
-	virtual void declareFunction(std::string _name, Sort _domain, Sort _codomain) = 0;
-	Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
+	virtual void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) = 0;
+	void declareFunction(std::string _name, Sort _domain, Sort _codomain)
+	{
+		declareFunction(std::move(_name), std::vector<Sort>{std::move(_domain)}, std::move(_codomain));
+	}
+	Expression newFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain)
 	{
 		declareFunction(_name, _domain, _codomain);
-		solAssert(_domain == Sort::Int, "Function sort not supported.");
 		// Subclasses should do something here
 		switch (_codomain)
 		{
 		case Sort::Int:
-			return Expression(std::move(_name), {}, Sort::IntIntFun);
+			return Expression(std::move(_name), {}, Sort::Int);
 		case Sort::Bool:
-			return Expression(std::move(_name), {}, Sort::IntBoolFun);
+			return Expression(std::move(_name), {}, Sort::Bool);
 		default:
 			solAssert(false, "Function sort not supported.");
 			break;