Getting asserted array indices

[Notselwyn]

Hi, when having a model generated by a z3 solver, is it possible to (quickly?) get all asserted indices? i.e. if there's somewhere in the constraint set an arr[123] == 456 / it is the output of the model, I want to extract (123, 456). Is there a way for this?

[Notselwyn]

I'm currently traversing the graph to get them, but unfortunately it seems some arrays with only 1 value get simplified to K(Int, 456) instead of z3.Store(Array, 123, 456). Is there a way to circumvent this simplification somewhere?