Different results in three ways to assgin values to an array in z3

[pastelblue]

As far as I know, there are three ways to assgin values to an array in z3.

1. use assert to assgin values to some of the cells:

(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))

(assert (= 1 (select a1 0)))
(assert (= 2 (select a2 0)))

z3 returns unsat when the constraint (assert (= a1 a2)) is added.

2. use as const to initialize the array first and then assgin values to specific cells:

(declare-const a3 (Array Int Int))
(assert
    (=
        (store ((as const (Array Int Int)) 64) 0 3)
        a3
    )
)
(declare-const a4 (Array Int Int))
(assert
    (=
        (store ((as const (Array Int Int)) 64) 0 4)
        a4
    )
)

Add (assert (= a3 a4)) and we obtain unsat again.

3. define the array via a function:

(define-const a5 (Array Int Int)
    (lambda ((i Int))
    (ite (= i 0) 5 64)))
(define-const a6 (Array Int Int)
    (lambda ((i Int))
    (ite (= i 0) 6 64)))

But if we add (assert (= a5 a6)), z3 returns sat. Why?
By the way, is there any (better) way to assign values to an array in z3?

[NikolajBjorner]

The last example exposes a bug on dealing with extensionality and lambda.
Z3 should have returned unsat (or unknown).
The first axiomatization tends to admit more efficient reasoning because search does not have to expand store-select axioms.