diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp
index 2ab494fc4..4e0ea7ef4 100644
--- a/libsolidity/formal/Predicate.cpp
+++ b/libsolidity/formal/Predicate.cpp
@@ -499,7 +499,15 @@ std::optional<std::string> Predicate::expressionToString(smtutil::Expression con
 	if (smt::isNumber(*_type))
 	{
 		solAssert(_expr.sort->kind == Kind::Int, "");
-		solAssert(_expr.arguments.empty(), "");
+		solAssert(_expr.arguments.empty() || _expr.name == "-", "");
+
+		if (_expr.name == "-")
+		{
+			solAssert(_expr.arguments.size() == 1);
+			smtutil::Expression const& val = _expr.arguments[0];
+			solAssert(val.sort->kind == Kind::Int && val.arguments.empty());
+			return "(- " + val.name + ")";
+		}
 
 		if (
 			_type->category() == Type::Category::Address ||