contract TestToken {
mapping(address => int) public balances;
constructor() public{
balances[msg.sender] = 10000;
}
// both should fail, however, actually
// it fails
function crytic_assert() view public returns (bool){
return false;
}
// it passes
function crytic_assert1(int xxx) view public returns (bool){
return false;
}
}
Execute manticore-verifier test.sol --contract TestToken
and it otuputs,
Honestly, it really astonished me. Why the obvious invalid assertion passes the verifier just after I add a useless argument xxx? Can anyone explain what happens?
Summary of the problem
Look at this minimal example
Execute
manticore-verifier test.sol --contract TestToken
and it otuputs,Honestly, it really astonished me. Why the obvious invalid assertion passes the verifier just after I add a useless argument
xxx
? Can anyone explain what happens?Manticore version
0.3.7
Python version
3.10.5
OS / Environment
Dependencies
Step to reproduce the behavior
Has given above.
Expected behavior
The two obviously invalid assertions should be rejected.
Actual behavior
The
crytic_assert1
indeed passes the check.Any relevant logs
None.