[555] % z3-4.8.5 model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
[556] % z3-4.8.6 model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
[557] % z3-4.8.7 model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
[558] % z3 model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
[559] % z3 smt.string_solver=z3str3 model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
[560] % 
[560] % cat small.smt2
(declare-fun s () String)
(assert (distinct (str.suffixof "B" (str.++ s "B")) (= s "")))
(check-sat)
[561] %