SMTChecker is unable to accurately determine the output of bytes.concat

[Subway2023]

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 test {
    function f() public {
        bytes memory a="1";
        bytes memory b="2";

        bytes memory c=bytes.concat(a,b);
        assert(c.length==2);
    }
}

solc test.sol --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0

[blishko]

This is another false positive due to overapproximations in the encoding. We will investigate if we can make the encoding more precise.