From f281c94b42564d6ac7f52909cc6640bca41b1f3a Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Tue, 4 Jun 2019 14:29:35 +0200
Subject: [PATCH] [SMTChecker] Test that non-Boolean literals are actually
 integers

---
 libsolidity/formal/CVC4Interface.cpp | 10 ++++++++--
 libsolidity/formal/Z3Interface.cpp   | 10 ++++++++--
 2 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index b46d8ec38..217aa816f 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -132,8 +132,14 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 		else if (n == "false")
 			return m_context.mkConst(false);
 		else
-			// We assume it is an integer...
-			return m_context.mkConst(CVC4::Rational(n));
+			try
+			{
+				return m_context.mkConst(CVC4::Rational(n));
+			}
+			catch (...)
+			{
+				solAssert(false, "");
+			}
 	}
 
 	solAssert(_expr.hasCorrectArity(), "");
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 20c7452b5..fdb04956e 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -131,8 +131,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		else if (n == "false")
 			return m_context.bool_val(false);
 		else
-			// We assume it is an integer...
-			return m_context.int_val(n.c_str());
+			try
+			{
+				return m_context.int_val(n.c_str());
+			}
+			catch (...)
+			{
+				solAssert(false, "");
+			}
 	}
 
 	solAssert(_expr.hasCorrectArity(), "");