From ae3350ae0320d140a427d2fa318e7002745a73a5 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leonardoaltt@gmail.com>
Date: Fri, 6 Apr 2018 18:01:40 +0200
Subject: [SMTChecker] Integration with CVC4

---
 libsolidity/formal/Z3Interface.cpp | 17 +----------------
 1 file changed, 1 insertion(+), 16 deletions(-)

(limited to 'libsolidity/formal/Z3Interface.cpp')

diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 125da00d..41943c92 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -116,21 +116,6 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 	for (auto const& arg: _expr.arguments)
 		arguments.push_back(toZ3Expr(arg));
 
-	static map<string, unsigned> arity{
-		{"ite", 3},
-		{"not", 1},
-		{"and", 2},
-		{"or", 2},
-		{"=", 2},
-		{"<", 2},
-		{"<=", 2},
-		{">", 2},
-		{">=", 2},
-		{"+", 2},
-		{"-", 2},
-		{"*", 2},
-		{"/", 2}
-	};
 	string const& n = _expr.name;
 	if (m_functions.count(n))
 		return m_functions.at(n)(arguments);
@@ -150,7 +135,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			return m_context.int_val(n.c_str());
 	}
 
-	solAssert(arity.count(n) && arity.at(n) == arguments.size(), "");
+	solAssert(_expr.hasCorrectArity(), "");
 	if (n == "ite")
 		return z3::ite(arguments[0], arguments[1], arguments[2]);
 	else if (n == "not")
-- 
cgit v1.2.3