From fb6fd1b3c25fd9c2bc9b8abb97fd150bc4ce219c Mon Sep 17 00:00:00 2001
From: Kevin Kelley <kevin@kelleysoft.com>
Date: Thu, 22 Nov 2018 08:02:25 +0800
Subject: add a 'readable' format for large hex values

---
 libsolidity/formal/SMTChecker.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

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

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 0c2af44b..17dc11ac 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -24,6 +24,8 @@
 
 #include <liblangutil/ErrorReporter.h>
 
+#include <libdevcore/StringUtils.h>
+
 #include <boost/range/adaptor/map.hpp>
 #include <boost/algorithm/string/replace.hpp>
 
@@ -300,14 +302,14 @@ void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _
 	checkCondition(
 		_value < minValue(_type),
 		_location,
-		"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
+		"Underflow (resulting value less than " + formatNumberReadable(_type.minValue()) + ")",
 		"<result>",
 		&_value
 	);
 	checkCondition(
 		_value > maxValue(_type),
 		_location,
-		"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
+		"Overflow (resulting value larger than " + formatNumberReadable(_type.maxValue()) + ")",
 		"<result>",
 		&_value
 	);
@@ -963,7 +965,7 @@ SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _exp
 		try
 		{
 			// Parse and re-format nicely
-			value = formatNumber(bigint(value));
+			value = formatNumberReadable(bigint(value));
 		}
 		catch (...) { }
 	}
-- 
cgit v1.2.3