Z3 prover: this Smtlib shoud not be SAT because last assert, why?

[willy3a]

`
(assert (= 1 1))
;(define-const 4 Int 4)
(declare-fun findMin ((Array Int Int) Int Int) Int)
(declare-fun isMin (Int (Array Int Int) Int Int) Bool)
(declare-const willy100 (Array Int Int))
(define-const aa (Array Int Int)(store (store (store (store (store
(store willy100 5 3) 0 7) 1 0) 2 1) 3 6) 4 2));701623

;--------assert findMin() return i~4
(assert (forall((i Int)) (=> (and (>= i 0) (< i 4))
(and (>= (findMin aa i 4) i) (< (findMin aa i 4) 4))
)))

;--------assert isMin()
(declare-const m Int) (assert (and (<= 0 m)(< m 4)))

(declare-const k Int) (assert (and (<= 0 k)(< k 4)))
(assert (forall ((i Int)(k Int))
(=> (and (<= 0 i) (< i 4) (isMin m aa i 4) )
(<= (select aa m)(select aa k))); aa[m]<=aa[k]
))

;-------assert: findMin(aa) => isMin(mi, aa)
(assert (forall ((i Int))
(=> (and (>= i 0) (< i 4) )
(let ((mi (findMin aa i 4))) ;
(isMin mi aa i 4)
))
))
;-------aa = [7,0,1,6,2,3]
(declare-const c_1 Int)
(assert (= c_1 (findMin aa 0 4)))
(declare-const c_2 Int)
(assert (= c_2 (findMin aa 2 4)))
(assert (= c_2 3));aa is [7,0,1,6,2,3], index should be 2 but is 3, why?

`