[SMTChecker] SMT logic error occurs when assigning values to fixed-size bytes array

[lum7na]

This seems to be related to #15701.

Compile: solc a.sol --via-ir --model-checker-invariants contract --model-checker-engine chc
Version: 0.8.29-develop.2025.1.21+commit.d750b9df.Linux.g++

contract c {
    function f(uint len) public returns (bytes memory) {
        bytes memory x = new bytes(len);
        for (uint i = 0; i < len; i++) {
            x[i] = bytes1(uint8(i));
        }
        return x;
    }
}

Output:

SMT logic error:
/solidity/libsmtutil/SolverInterface.h(233): Throw in function static solidity::smtutil::Expression solidity::smtutil::Expression::store(solidity::smtutil::Expression, solidity::smtutil::Expression, solidity::smtutil::Expression)
Dynamic exception type: boost::wrapexcept<solidity::smtutil::SMTLogicError>
std::exception::what: SMT assertion failed
[solidity::util::tag_comment*] = SMT assertion failed