[580] % z3 small.smt2 
unsat
[581] % z3 smt.string_solver=z3str3 small.smt2 
sat
[582] % cat small.smt2 
(declare-fun a () String)
(declare-fun b () Int)
(assert (distinct (str.substr (str.replace "B" a "A") b b)
     (str.substr "B" 0 (str.indexof "A" a b))))
(check-sat)
[583] %