It seems from the question that you can use proper let expressions. Then it will be easier for Z3:
(declare-datatypes ()
((mystruct (mk-mystruct
(array-fld (Array Int Int))
(blist-fld (List Bool))))))
(define-fun array-fld-upd ((v (Array Int Int)) (obj mystruct)) mystruct
(mk-mystruct v (blist-fld obj)))
(define-fun blist-fld-upd ((v (List Bool)) (obj mystruct)) mystruct
(mk-mystruct (array-fld obj) v))
(push)
(assert
(forall ((z0 mystruct))
(let ((array-val (array-fld z0)))
(= (select (array-fld
(array-fld-upd (store array-val 2 4) z0)) 3)
(select (array-fld z0) 3)))))
(check-sat)