[619] % z3release small.smt2
unsat
(error "line 14 column 10: model is not available")
[620] % cvc5 -q --strings-exp --produce-models --check-models small.smt2
sat
(
(define-fun a () String "")
)
[621] % 
[621] % cat small.smt2
(declare-fun a () String)
(assert
 (xor
  (= (= (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B")
      (str.replace "B" (str.replace "B" a (str.++ a "B")) a))
   (not
    (= (str.replace "B" (str.replace a "B" "") "B")
     (str.replace "B" a (str.++ a "B")))))
  (= (str.replace "B" a "")
   (str.replace "B" a
    (ite (not (= (str.replace "" (str.replace a "" a) "") "")) ""
     (str.replace "" (str.replace a "B" "") "B"))))))
(check-sat)
(get-model)
[622] %