Unable to verify non-decreasing balance.

[michael-emmi]

$ cat a.sol && solc-verify.py a.sol 
pragma solidity ^0.5.0;

contract A {

    /// @notice postcondition address(this).balance >= __verifier_old_uint(address(this).balance)
    function f1() public payable { }

}
A::f1: ERROR
 - a.sol:6:5: Postcondition 'address(this).balance >= __verifier_old_uint(address(this).balance)' might not hold at end of function.
A::[implicit_constructor]: OK
Errors were found by the verifier.

[hajduakos]

In the default integer mode, msg.value is also an integer and can be negative. Try running with --arithmetic mod. We were thinking about adding constraints for non-negative integers on a best effort basis. However, now the semantics of the integer mode is clear, everything is an unbounded, signed integer. As soon as we start adding such constraints, it might be hard to keep track. But I am not against it, as it makes the integer mode more precise. @dddejan ?

[dddejan]

We should just move the default integer encoding to mod.

[michael-emmi]

It succeeds with --artihmetic mod, but why should it work actually (?) when the pre-value of balance could be so large so that the post-value overflew. Looking again, I would have expected a precondition that balance and msg.value are not too large.

[hajduakos]

In --arithmetic mod we do have implicit assumptions that balances cannot overflow.