(set-logic QF_S)
(declare-fun var0 () String)
(assert (= (str.++ "nk^" var0) (str.++ var0 "ROA")))
(check-sat)