cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Negative numbers do not have to be atoms

Browse Source
This commit is contained in:
Martin Blicha 2023-07-27 14:40:05 +02:00
parent 779db2d84f
commit 4b50f26834
1 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libsolidity/formal/Predicate.cpp
View File

@ -499,7 +499,15 @@ std::optional<std::string> Predicate::expressionToString(smtutil::Expression con
if (smt::isNumber(*_type)) if (smt::isNumber(*_type))
{ {
solAssert(_expr.sort->kind == Kind::Int, ""); 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 ( if (
_type->category() == Type::Category::Address || _type->category() == Type::Category::Address ||