[592] % z3release small.smt2
unsat
unsat
[593] % cvc5 -q --strings-exp --dump-models --check-models small.smt2
sat
(
(define-fun a () String "AA")
)
unsat
[594] % 
[594] % cat small.smt2
(declare-fun a () String)
(assert (> (str.indexof a "" (* 2 (str.len a))) 0))
(check-sat)

(reset)

(define-fun a () String "AA")
(assert (> (str.indexof a "" (* 2 (str.len a))) 0))
(check-sat)
[595] %