why first is SAT, but sencond is not SAT?

[willy3a]

The meaning of findMin (aa, i, j) is to find and return the index of minimum value between aa[i] and aa[j].

May I ask, why it is satisfied?

(declare-fun findMin ((Array Int Int) Int Int) Int)
(assert (forall((i Int)) (=> (and (>= i 0) (< i 4))
    (forall ((bb (Array Int Int)))
    (and (< (findMin bb i 4) 4))
        ))))

and this is SAT.

(declare-fun findMin ((Array Int Int) Int Int) Int)
(assert (forall((i Int)) (=> (and (>= i 0) (< i 4))
    (forall ((aa (Array Int Int)))
       (>= (findMin aa i 4) i)
    ))))

But, why this is not satisfied?

(declare-fun findMin ((Array Int Int) Int Int) Int)
(assert (forall((i Int)) (=> (and (>= i 0) (< i 4))
    (forall ((bb (Array Int Int)))
    (and (>= (findMin bb i 4) i)
            (< (findMin bb i 4) 4))
        ))))

[NikolajBjorner]

z3 returns unknown for the second formula. You can run z3 using the option sat.smt=true and it then returns sat.
Quantifier reasoning is not complete.