From ac398869ad8ab1191f5c52fc58703877e3766ebc Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Wed, 7 Feb 2024 12:38:41 +0100 Subject: [PATCH] SMTChecker: Respect signedness of integer type When creating zero-value expression, we need to respect the signedness of the passed type. --- libsolidity/formal/SymbolicTypes.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 45b872b3d..350e18bdc 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -476,7 +476,7 @@ smtutil::Expression zeroValue(frontend::Type const* _type) if (isSupportedType(*_type)) { if (isNumber(*_type)) - return 0; + return isSigned(_type) ? smtutil::Expression(s256(0)) : smtutil::Expression(static_cast(0)); if (isBool(*_type)) return smtutil::Expression(false); if (isArray(*_type) || isMapping(*_type))