Replace Arrays With Uninterpreted Functions in the SMT encodings

[d-xo]

We currently use nested and constant arrays which severly limits the solvers we can use (currenlty only Z3). If we instead use UF's with axioms, we can use cvc5, bitwuzla, yices and stp, all of which should be more performant than Z3.

[msooseth]

I'm closing because (1) we can nowadays use many more SMT solvers and (2) @blishko is working on some form of UF system that may allow us to even have symbolic sized copyslice. I think that issue/PR is a better place to discuss and work on this. Issue: #492