From 4098661b89264439ce31be6a1372f89aaf0cb1e5 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 23 Jun 2022 15:18:26 +0200
Subject: [PATCH] Fix guessing of numbers.

---
 libsolutil/BooleanLP.cpp |  5 ++++-
 tools/solsmt.cpp         | 13 ++++++++++++-
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index bf7cb9638..595de5080 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -640,7 +640,10 @@ namespace
 {
 bool isNumber(string const& _expr)
 {
-	return !_expr.empty() && (isDigit(_expr.front()) || _expr.front() == '.');
+	for (char c: _expr)
+		if (!isDigit(c) && c != '.')
+			return false;
+	return true;
 }
 rational parseRational(string const& _atom)
 {
diff --git a/tools/solsmt.cpp b/tools/solsmt.cpp
index c8f72df84..6750548bd 100644
--- a/tools/solsmt.cpp
+++ b/tools/solsmt.cpp
@@ -129,13 +129,24 @@ string_view command(SMTLib2Expression const& _expr)
 	return get<string_view>(items.front().data);
 }
 
+namespace
+{
+bool isNumber(string_view const& _expr)
+{
+	for (char c: _expr)
+		if (!isDigit(c) && c != '.')
+			return false;
+	return true;
+}
+}
+
 smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<string, SortPointer> const& _variableSorts)
 {
 	return std::visit(GenericVisitor{
 		[&](string_view const& _atom) {
 			if (_atom == "true" || _atom == "false")
 				return Expression(_atom == "true");
-			else if (isDigit(_atom.front()) || _atom.front() == '.')
+			else if (isNumber(_atom))
 				return Expression(string(_atom), {}, SortProvider::realSort);
 			else
 				return Expression(string(_atom), {}, _variableSorts.at(string(_atom)));