[682] % z3release rewriter.flat=false smt.threads=2 model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
[683] %
[683] % cat small.smt2
(declare-fun s () String)
(assert (str.contains (str.substr (str.replace (str.substr s 0 (+ (str.indexof s "a" 0) 1)) "a" "b") 1 (str.len s)) "c"))
(check-sat)
[684] %