$bin/z3-145ec8f model_validate=true bug.smt2
sat
(error "line 2 column 10: an invalid model was generated")
(model 
)
$cat bug.smt2 
(assert (= (seq.indexof (seq.unit 0) (seq.unit 0)) 0))
(check-sat)
(get-model)