SMTChecker: Incorrectly determines insufficient balance.

[Subway2023]

Description

When the transfer amount is 0, SMTChecker incorrectly determines insufficient balance

Environment

• Compiler version:
• Target EVM version (as per compiler settings):
• Framework/IDE (e.g. Truffle or Remix):
• EVM execution environment / backend / blockchain client:
• Operating system:

Steps to Reproduce

contract C{
    address payable recipient;
    uint amount=0;

    function f() public {
        uint tempAmount = address(this).balance ;
        recipient.transfer(tempAmount);
        recipient.transfer(amount);
    }
}

solc-0825 C.sol --model-checker-engine all

[blishko]

This is again the problem with BMC not tracking the state of the contract. Since it is doing only a local check, it does not know that the state variable amount is always 0 and cannot change. So this is not a bug, but false positive due to BMC's over-approximating modeling.

The problem is that CHC currently does not attempts to verify the verification target Insufficient funds for transfer. But maybe it should.