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