SMTChecker: Unable to correctly determine the result of function pointer comparison

[Subway2023]

Description

When comparing two internal functions, the SMTChecker is unable to determine the comparison result correctly.

Environment

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

Steps to Reproduce

contract C {
    function f() internal {}
    function g() internal {}

    function test() public {
        assert(C.f != C.g);
    }
}

Remix

Execute normally, no revert

SMTChecker

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

[blishko]

Function pointers are not supported in SMTChecker and it issues a warning about that on this example:
Warning: SMTChecker: 1 unsupported language feature(s). Enable the model checker option "show unsupported" to see all of them.

Moreover, the compiler also issues a warning that comparison of internal function pointers will be disallowed in the next breaking release:
Warning: Comparison of internal function pointers can yield unexpected results in the legacy pipeline with the optimizer enabled, and will be disallowed entirely in the next breaking release.

Since SMTChecker over-approximates in the presence of unsupported features, the assertion violation warning is to be expected.