SMTChecker: Unable to accurately describe the balance

[Subway2023]

Description

Unable to correctly determine that the current balance is 0 after transferring out all balances.

Environment

• Compiler version: 0.8.25
• Target EVM version (as per compiler settings): No restrictions
• Framework/IDE (e.g. Truffle or Remix): Command-line
• EVM execution environment / backend / blockchain client: None
• Operating system: Linux

Steps to Reproduce

contract C{
  address payable recipient;
  function f() public {
      bool success = recipient.send(address(this).balance);
      if (success) {
          assert(address(this).balance==0);
      }
  }
}

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

[blishko]

If you add the assumption that the recipient is different from the sender, require(recipient != address(this));, SMTChecker will prove that assertion holds.

While we could improve the analysis for this particular example, it is also not very realistic, because recipient here is always 0.
In general, you would want to make sure that you are not sending to yourself.