Meaning of Ext in ModelRef (Python API)

[walnutwaldo]

What I dump a ModelRef as such:
print(solver.model())
I sometimes get these weird Ext items at the end:

[create_unknown_t2_a = 0,
...
 call_count = K(BitVec(160), 0),
 Ext = [else -> 2],
 keccak256_424 = [else -> 0],
 Ext = [else -> 0]]

Looking into it closer, I could find that these declarations are actually named array-ext. But what is the significance of these items? For the most part, I have enough information to be able to understand a counterexample being constructed in a ModelRef but I want to make sure I'm not missing something important.

[NikolajBjorner]

The array-ext function is actually internal to the array theory. It takes two arrays and returns an index. If the two arrays are equal, the index is arbitrary. If the two arrays are different, then selecting at that index results in two different values.
Since your input probably doesn't use Ext you can ignore these entries for your purposes.

[walnutwaldo]

Thank you for the explanation!