From e2959ce55ce22b32b08bd36015596cd2bda77bd7 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Tue, 11 May 2021 14:07:02 +0200
Subject: [PATCH] Assign cast from constants directly

---
 libsolidity/formal/SMTEncoder.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index bc53c7126..36b07f0a5 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1113,6 +1113,14 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 	{
 		solAssert(smt::isNumber(*funCallType), "");
 
+		RationalNumberType const* rationalType = isConstant(*argument);
+		if (rationalType)
+		{
+			// The TypeChecker guarantees that a constant fits in the cast size.
+			defineExpr(_funCall, symbArg);
+			return;
+		}
+
 		auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType);
 		auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
 		if (fixedCast && fixedArg)