SMTChecker: Unable to support keccak256 well

[Subway2023]

Description

0.7.4 release claims that the SMTChecker supports the keccak256 function. However, SMTChecker cannot accurately assess the output value of keccak256.

Environment

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

Steps to Reproduce

contract C {
    function f() public {
        bytes memory t0="1";
        bytes memory t1="1";
        bytes32 a=keccak256(t0);
        bytes32 b=keccak256(t1);
        assert(a==b);
    }
}

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

The SMTChecker is experiencing false positives.