`access-out-of-bounds-array` may return different model

For the test `access-out-of-bounds-array` we check for accesses out of bounds and we require that the returned model has `x > 1`, since the array has at least length 2.

https://github.com/ethereum/hevm/blob/533b655804909ba0ef172405d79ca8f920e36a64/test/test.hs#L549-L563

However, adding the constraint `x <= 1` does not make the query unsatisfiable. If the initial length of the array before the two pushes is `maxInt256 `, then `1 = 2 + length_arr`. Therefore, depending on the size of the initial array, `x = 0` or `x = 1` can also be returned as counterexamples. However, these are not real counterexamples, since these accesses are not really out of bounds.

Start with test/test.hs lines 549-563 and reproduce the access-out-of-bounds-array query. Inspect how the initial array length and the two pushes affect the returned model, particularly cases where x is 0 or 1. Done means the test no longer treats these non-real counterexamples as valid out-of-bounds counterexamples.

Written by the indexing model from the issue text.