1 files changed, 18 insertions, 2 deletions
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index a6c1f87c..54542233 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -64,9 +64,12 @@ void SMTLib2Interface::pop()
 	m_accumulatedOutput.pop_back();
 }
 
-void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void SMTLib2Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
 {
 	// TODO Use domain and codomain as key as well
+	string domain("");
+	for (auto const& sort: _domain)
+		domain += toSmtLibSort(sort) + ' ';
 	if (!m_functions.count(_name))
 	{
 		m_functions.insert(_name);
@@ -74,7 +77,7 @@ void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomai
 			"(declare-fun |" +
 			_name +
 			"| (" +
-			(_domain == Sort::Int ? "Int" : "Bool") +
+			domain +
 			") " +
 			(_codomain == Sort::Int ? "Int" : "Bool") +
 			")"
@@ -140,6 +143,19 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
 	return sexpr;
 }
 
+string SMTLib2Interface::toSmtLibSort(Sort _sort)
+{
+	switch (_sort)
+	{
+	case Sort::Int:
+		return "Int";
+	case Sort::Bool:
+		return "Bool";
+	default:
+		solAssert(false, "Invalid SMT sort");
+	}
+}
+
 void SMTLib2Interface::write(string _data)
 {
 	solAssert(!m_accumulatedOutput.empty(), "");