Soundness bug with quantifies & recursion over Int arrays

[SaswatPadhi]

Z3 reports sat on the following formula, and unsat after a simple simplification (commented below):

(set-logic ALL)

(define-fun-rec is_histogram ( (src (Array Int Int))
                               (N Int)
                               (N_MAX Int)
                               (result (Array Int Int)) )
                             Int
  (ite (<= N 0)
       (ite (forall ((k Int)) (=> (= 0 k)
                                  ; `sat` with select `k`, unsat with select `0`
                                  (= (select result k) 0)))
            1
            0)
      0)
)
(define-const |is_histogram::N!0@1#1| Int 0)
(define-const |is_histogram::N_MAX!0@1#1| Int 1)
(define-const |symex_dynamic::dynamic_object1#1| (Array Int Int) ((as const (Array Int Int)) 0))
(define-const |symex_dynamic::dynamic_object2#1| (Array Int Int) (store ((as const (Array Int Int)) 10)
       0
       0))
(assert (not (= 1
     (is_histogram |symex_dynamic::dynamic_object1#1|
                   |is_histogram::N!0@1#1|
                   |is_histogram::N_MAX!0@1#1|
                   |symex_dynamic::dynamic_object2#1|))))
(check-sat)

CVC4 reports unsat: https://cvc4.github.io/app/#temp_3e93feef-3a35-4b6d-8c87-6892265c9a6e

[NikolajBjorner]

Quantifiers in recursive definitions won't be supported until sat.euf=true is stable.