Incorrect model with sequences

[LeventErkok]

This benchmark is indeed SAT, but z3 returns an invalid model; and it knows about it:

(set-option :produce-models true)
(set-logic ALL)
(define-fun s2 () Int 2)
(define-fun s4 () Int 0)
(define-fun s5 () Int 1)
(declare-fun s0 () (Seq (_ BitVec 16)))
(define-fun s1 () Int (seq.len s0))
(define-fun s3 () Bool (>= s1 s2))
(define-fun s6 () (Seq (_ BitVec 16)) (seq.extract s0 s4 s5))
(define-fun s7 () Int (- s1 s5))
(define-fun s8 () (Seq (_ BitVec 16)) (seq.extract s0 s7 s5))
(define-fun s9 () Bool (distinct s6 s8))
(define-fun s10 () Bool (and s3 s9))
(assert s10)
(check-sat)

We have:

$ z3 model_validate=true a.smt2
sat
(error "line 15 column 10: an invalid model was generated")

Recent breakage.