SMTChecker: Fail to parse abi.encodeCall

[Subway2023]

Description

0.8.14 release claims that the SMTChecker supports the abi.encodeCall. However, when using abi.encodeCall to encode function, SMTChecker will crash

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()public {
        bytes memory result=abi.encodeCall(this.f, ());
        assert(result.length==4);
    }
}

Remix

Successfully executed.

Command-line

solc C.sol --model-checker-ext-calls trusted --model-checker-timeout 0 --model-checker-engine chc --model-checker-solvers z3

or

solc C.sol --model-checker-ext-calls trusted --model-checker-timeout 0 --model-checker-engine bmc --model-checker-bmc-loop-iterations 10 --model-checker-solvers z3

SMTChecker crash