solidity/test/libsolidity/smtCheckerTests/types/address_transfer.sol
2019-05-02 12:05:21 +02:00

16 lines
345 B
Solidity

pragma experimental SMTChecker;
contract C
{
function f(address payable a) public {
uint x = 100;
require(x == a.balance);
a.transfer(600);
// This fails since a == this is possible.
assert(a.balance == 700);
}
}
// ----
// Warning: (131-146): Insufficient funds happens here
// Warning: (195-219): Assertion violation happens here