SMTChecker: Unable to accurately determine the modification of global variables by functions called using call()

[Subway2023]

Description

When a function called using call() modifies global variables, SMTChecker is unable to determine the final value of the global variables

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

contract Caller {
  int a;
  function f() public {
      a=1;
  }
  function g()public{
      bytes memory payload=abi.encodeWithSignature("f()");
      address(this).call(payload);
      assert(a==1);
  }
}

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

[blishko]

SMTChecker cannot model precisely what ABI methods like encodeWithSignature compute.
To stay sound, it over-approximates the possible behaviour.
This means that it only models the basic functional property: they yield equal output for equal inputs.
Otherwise, it assumes that the result can be any value.

Similarly, it over-approximates the behaviour of call method. This can potentially call any external code, which can do anything.
This over-approximating modeling results in false positives that you see in this issue, but keeps the encoding sane.