Multi-Dimensional Array Solving and Models Broken for CVC4, Yices2, Bitwuzla, Boolector, and Princess

[baierd]

Multi-Dimensional array solving and/or model generation is broken for several solvers. For Princess this is already known and a issue exists here: #520.
See tests added here.

We should fix Bitwuzla ASAP, as it is used quite a lot. The others can be tackled together with #525 that identified a lot of issues in general with array models.

(Sub-issues need to be created for the fixes!)