Soundness bug with quantifies & recursion over BV 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 (_ BitVec 64) (_ BitVec 8)))
                               (N (_ BitVec 64))
                               (N_MAX (_ BitVec 64))
                               (result (Array (_ BitVec 64) (_ BitVec 8))) )
                             (_ BitVec 8)
  (ite (bvsle N (_ bv0 64))
       (ite (forall ((k (_ BitVec 64))) (=> (= (_ bv0 64) k)
                                            ; `sat` with select `k`, `unsat` with select `(_ bv0 64)`
                                            (= (select result k) (_ bv0 8))))
            (_ bv1 8)
            (_ bv0 8))
       (_ bv0 8))
)

(define-const |is_histogram::N!0@1#1| (_ BitVec 64) #x0000000000000000)
(define-const |is_histogram::N_MAX!0@1#1| (_ BitVec 64) #x0000000000000001)
(define-const |symex_dynamic::dynamic_object1#1| (Array (_ BitVec 64) (_ BitVec 8)) ((as const (Array (_ BitVec 64) (_ BitVec 8))) #x00))
(define-const |symex_dynamic::dynamic_object2#1| (Array (_ BitVec 64) (_ BitVec 8)) (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) #x10)
       #x0000000000000000
       #x00))
(assert (not (= (_ bv1 8)
     (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_8ab1106b-833c-49b6-b3ad-496ce0da6adb

(might be related to #5377)

[NikolajBjorner]

won't be supported until sat.euf=true option is stable.