[576] % z3 model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
(model 
 (define-fun a () String
  "")
)
[577] % 
[577] % cat small.smt2
(declare-fun a () String)
(assert (distinct (distinct a "A") (str.suffixof "A" (str.replace "A" a "B" ))))
(check-sat)
(get-model)
[578] %