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

## 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
```solidity
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
```