The Z3 tutorial (Section Quantifiers) describes for which fragments Z3 is complete. The general problem is undecidable.
Regarding your example, Z3 will fail on satisfiable instances that contain quantifiers ranging over arrays. Note that your formula is satisfiable. If we negate it, then Z3 automatically proves it to be unsatisfiable.
(assert (not (forall ((a (Array Int Int)) (b (Array Int Int)))
(=> (forall ((i Int)) (= (select a i) (select b i))) (= a b)))))
(check-sat)
Remark: Z3 is essentially a satisfiability checker. To prove a formula F
, we show that the negation is unsatisfiable.