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