It might be interesting to benchmark this to see how expensive computing the dual representation on demand every time is and whether it might be worth saving the offset together with the offset representation so it can be a simple lookup.

There is still one issue remaining with addresses of arrays that were casted to a different type, and where then an offset is taken:

To handle this correctly, one would have to track the type of the pointer to the abstract address operations, so that one can compute the correct offset in bits from it.

As discussed with @michael-schwarz, one approach to handle the issue described in the previous comment, would be to introduce a separate constructor for broken / corrupted abstract offsets.

The idea is to set the offset to CorruptedOffset in Base, when an offset is added on a pointer, where the static pointer-target type is different from the type of the actual abstract target.
Then, abstract equality checks of two address that have the same base-address, and at least one of the addresses has a CorruptedOffset will result in Unknown. When reading from an address with corrupted offset, the top_value of the type would be read, while writing would set the whole base-value to the top_value of the type.

I started some work on this in a separate branch: array_cast_broken_offsets. There are some failing test cases with the changes from that branch, mostly caused by reduced precision.

To handle this correctly, one would have to track the type of the pointer to the abstract address operations, so that one can compute the correct offset in bits from it.

I would've expected the abstract bitsOffset calculation to handle that already, does it not? I think Cil.bitsOffset correctly accounts for array element type sizes on index offsets.