invalid model on QF_ABV formula

[zhendongsu]

It might be related to #5345.

[620] % z3release model_validate=true small.smt2
sat
(error "line 9 column 39: an invalid model was generated")
[621] % cat small.smt2
(set-option :rewriter.expand_nested_stores true)
(declare-fun a () (_ BitVec 1))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun c () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun d () (_ BitVec 1))
(assert (= (_ bv1 32) ((_ zero_extend 31) a)))
(assert (= d (bvcomp (_ bv0 32) ((_ zero_extend 24) (select c (_ bv0 32))))))
(assert (= c (store (store (store b (_ bv1 32) (_ bv0 8)) (_ bv0 32) (_ bv0 8)) ((_ zero_extend 31) a) (_ bv1 8))))
(check-sat-using (then qfnra-nlsat smt))