Invalid model for string formula

[rainoftime]

Hi, for the following formula,
z3 3bca1fb

(declare-fun a () (Seq Int))
(declare-fun b () (Seq Int))
(declare-fun c () (Seq Int))
(declare-fun x () Int)
(declare-fun y () Int)
(assert (or (= b c) (= a c)))
(assert (= (seq.nth c 0) (seq.nth c x)))
(assert (not (= (seq.nth b y) (seq.nth c y))))
(check-sat)
(get-model)

./z3 model_validate=true ../delta.out.smt2 
sat
(error "line 9 column 10: an invalid model was generated")
(
  (define-fun b () (Seq Int)
    (seq.unit 0))
  (define-fun c () (Seq Int)
    (seq.unit 0))
  (define-fun a () (Seq Int)
    (seq.unit 0))
  (define-fun x () Int
    (- 1))
  (define-fun y () Int
    (- 7720))
  (define-fun seq.nth_u ((x!0 (Seq Int)) (x!1 Int)) Int
    (ite (and (= x!0 (seq.unit 0)) (= x!1 (- 7720))) 21239
      0))
)