z3 fails to recognize that some SMT-LIB Logics include arrays

[BrunoDutertre]

There's a long list of logic names used in SMT-LIB benchmarks at https://zenodo.org/records/11061097.
Several of them include quantifiers and arrays: from ABV to AUFNIRA.

Recent versions of z3 do not recognize that many of these need arrays and can fail on examples in these logics
(and produce incorrect answers).

Here's an example:

(set-logic AUFDTLIRA)
(declare-const a (Array Int Real))
(declare-const i Int)
(assert (forall ((k Int)) (> (select a k) 0)))
(assert (= (select a i) 0))
(check-sat)

On this: z3-4.14.x will produce:

(error "line 2 column 18: unknown sort 'Array'")
(error "line 4 column 37: unknown constant a")
(error "line 5 column 19: unknown constant a")
sat

Older releases ignored the logic and produced the right answer:

./z3-4.13.0 test_aufdtlira.smt2
unsupported
; ignoring unsupported logic AUFDTLIRA line: 1 position: 1
unsat