Incorrect array equivalence result

[RobinWebbers]

Whilst toying with array theories, I noticed that the array equivalence is broken. Consider the following example where we compare two arrays that are not equal:

(define-const a1 (Array Bool Int) (store ((as const (Array Bool Int)) 0) true 1))
(define-const a2 (Array Bool Int) ((as const (Array Bool Int)) 1))
(assert (= a1 a2))
;(assert (= (select a1 false) (select a2 false)))
(check-sat)

Here, z3 will return sat. Uncommenting the assertion for the index false will make the check unsat (as it should be). I'm not sure if Z3 is expected to handle such equalities in the first place, but I guess returning "unknown" would be better if this is the case.