invalid model

[LeventErkok]

$ cat a.smt2
(set-logic ALL)

(declare-fun x () (Seq String))

(define-fun-rec f ((s (Seq String))) String
    (ite (= (seq.len s) 0)
    	 ""
	 (str.++ (seq.nth s 0) (f (seq.extract s 1 (- (seq.len s) 1))))))

(assert (>= (str.len (f x)) 5))
(check-sat)
(get-model)

$ z3 model_validate=true a.smt2
sat
(error "line 11 column 10: an invalid model was generated")
(
  (define-fun x () (Seq String)
    (seq.unit ""))
  (define-fun seq.nth_u ((x!0 (Seq String)) (x!1 Int)) String
    "")
)