`hevm symbolic`: Spurious Counterexample

`hevm symbolic` produces a spurious counterexample for a program compiled with `solx`:

```
Using assertion code(s): 1

Discovered the following 1 counterexample(s):

Calldata:
0xb96657ca0000000000000000000000000000000000000000000000000000000000000001
Storage:
Addr SymAddr "entrypoint": []
Addr SymAddr "miner": []
Transaction Context:
TxValue: 0x0
Addrs:
SymAddr "entrypoint": 0xBf06000000781D10Ca00b184562e9c3aF4A5fCE6
SymAddr "miner": 0xBcFdFFfF9BBbE0fb305b0d609E7C833BA4cdFcDd
SymAddr "origin": 0x4302000064441f04cFA4F29f61837Cc45b320322
```

This counterexample cannot be reproduced when running the compiled bytecode concretely using go-ethereum (which leads me to believe it isn't an issue on the `solx` side).

### Program
```
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.0;

// evm osaka, viaIR, optimizer mode z.
contract PlaceholderContract {
bool private s2;
uint256[] private b1;
bool[] private b2;

function check_entrypoint(bool x) public {
unchecked {
uint256 k1 = b1.length;
uint256 k2 = b2.length;
b1.push(1);
b2.push(true);
b2.push(true);
uint256 t4 = x ? 2 : 3;
s2 = (b1[k1] < t4);
bool t5 = (s2 ? b2[k2] : b2[k2 + 1]);
assert(t5);
}
}
}
```

or equivalently in the standard JSON format including the necessary compile options
```
{
"language": "Solidity",
"sources": {
"target.sol": {
"content": "// SPDX-License-Identifier: UNLICENSED\npragma solidity ^0.8.0;\n\n// solx 72e0a558, evm osaka, viaIR, optimizer mode z.\n// b2 == [true, true], so `t5` is true on BOTH ternary branches and the assert\n// can never fail. solx-compiled code lets hevm reach the assertion violation.\ncontract PlaceholderContract {\n bool private s2;\n uint256[] private b1;\n bool[] private b2;\n\n function check_entrypoint(bool x) public {\n unchecked {\n uint256 k1 = b1.length;\n uint256 k2 = b2.length;\n b1.push(1);\n b2.push(true);\n b2.push(true);\n uint256 t4 = x ? 2 : 3;\n s2 = (b1[k1] < t4);\n bool t5 = (s2 ? b2[k2] : b2[k2 + 1]);\n assert(t5);\n }\n }\n}\n"
}
},
"settings": {
"evmVersion": "osaka",
"viaIR": true,
"optimizer": {
"mode": "z"
},
"outputSelection": {
"*": {
"*": [
"evm.deployedBytecode.object"
]
}
}
}
}
```

hevm is called with `hevm symbolic --smt-timeout 10 --num-solvers 1 --code "$CODE" --initial-storage Empty`. I am using version `0.58.0 [no git revision present]` with z3 (but it is also reproducible with cvc5).

Bytecode for reference: https://gist.github.com/sbauer00/f71ee7594dc2bd368d266e3ec15f9c89

Start with the supplied Solidity program, standard JSON, and reference bytecode, then run the reported `hevm symbolic --smt-timeout 10 --num-solvers 1 --code "$CODE" --initial-storage Empty` command using hevm 0.58.0. Trace the `hevm symbolic` entry point to determine why the assertion is reported as violated; done means the compiled example no longer yields a spurious counterexample.

Written by the indexing model from the issue text.