Strange result for arrays and datatypes when using OCaml API

Question

I am using Z3 via Ocaml binding. For the following formula

(set-info :status unknown)
(set-logic ALL)
(declare-datatypes ((Loc 0)) (((|1|) (|2|) (|3|) (|4|) (|5|))))
 (declare-fun z () Loc)
(declare-fun y () Loc)
(declare-fun x () Loc)
(declare-fun nil () Loc)
(declare-fun |global fp| () (Array Loc Bool))
(declare-fun heap () (Array Loc Loc))
(declare-fun footprint0 () (Array Loc Bool))
(declare-fun heap0 () (Array Loc Loc))
(declare-fun footprint1 () (Array Loc Bool))
(declare-fun footprint4 () (Array Loc Bool))
(declare-fun footprint3 () (Array Loc Bool))
(declare-fun footprint2 () (Array Loc Bool))
(assert
 (let (($x59 (select |global fp| nil)))
 (let (($x60 (not $x59)))
 (let ((?x61 (select heap nil)))
 (let (($x62 (= nil ?x61)))
 (let (($x58 (= footprint0 |global fp|)))
 (let (($x96 (forall ((l!0 Loc) )(let (($x49 (= (select heap l!0) (select heap0 l!0))))
 (or (not (select footprint0 l!0)) $x49)))
 ))
 (let ((?x20 ((as const (Array Loc Bool)) false)))
 (let ((?x38 (store ?x20 y true)))
 (let (($x39 (= footprint4 ?x38)))
 (let (($x28 (= footprint1 footprint3)))
 (let (($x27 (= footprint1 footprint2)))
 (let (($x32 (or $x27 $x28)))
 (let (($x26 (= footprint3 ?x20)))
 (let ((?x21 (store ?x20 x true)))
 (let (($x22 (= footprint2 ?x21)))
 (let ((?x36 (select heap0 y)))
 (let (($x37 (= ?x36 z)))
 (and 
  (or $x28 (and (= (select heap0 x) y) $x27)) 
  $x37 
  (= ((_ map and ) footprint1 ((_ map not ) footprint4)) ?x20) 
  $x22 $x26 $x32 $x39 
  (= footprint0 ((_ map and ) footprint4 ((_ map not ) footprint1))) 
  $x96 $x58 $x62 $x60 
  (not (= nil |5|)) (not (= x |5|)) (not (= y |5|)) (not (= z |5|))
)))))))))))))))))))
(check-sat)

I got the following model:

(define-fun footprint4 () (Array Loc Bool)
  (store ((as const (Array Loc Bool)) true) |2| false))
(define-fun x () Loc 
  |1|)
(define-fun footprint0 () (Array Loc Bool)
  (store (store ((as const (Array Loc Bool)) true) |1| false) |2| false))
(define-fun footprint3 () (Array Loc Bool)
  (store (store ((as const (Array Loc Bool)) true) |1| false) |2| false))
(define-fun z () Loc 
  |1|)
(define-fun nil () Loc 
  |1|)
(define-fun |global fp| () (Array Loc Bool)
  (store (store ((as const (Array Loc Bool)) true) |1| false) |2| false))
(define-fun y () Loc 
  |1|)
(define-fun heap () (Array Loc Loc)
  (store ((as const (Array Loc Loc)) |1|) |2| |2|))
(define-fun footprint1 () (Array Loc Bool)
  (store ((as const (Array Loc Bool)) true) |2| false))
(define-fun footprint2 () (Array Loc Bool)
  (store ((as const (Array Loc Bool)) true) |2| false))
(define-fun heap0 () (Array Loc Loc)
  ((as const (Array Loc Loc)) |1|))

I think that the result is incorrect because the formula asserts that array footprint3 is a constant array of false values (expressions ?x20 and $x26). But in the model, for example, footprint3[|3|] is true.

Is the model indeed incorrect, or is there some aspect of combining datatypes with arrays that I am missing?

Also, when storing formula to a file and running Z3 from the command line, I will obtain an expected model. Therefore I was not able to minimize the example.