1 2 3 4 5 6 7 8 9 10
(set-info :smt-lib-version 2.5) (set-logic ALL) (set-info :status sat) (set-option :strings-exp true) (set-option :strings-fmf true) (set-option :produce-models true) (declare-fun x () String) (assert (= (str.len (str.replaceall x "B" "CC")) (+ (str.len x) 2))) (assert (> (str.len x) 2)) (check-sat)