1 2 3 4 5 6 7 8 9 10 11 12 13
(set-logic ALL_SUPPORTED) (set-info :status sat) (declare-fun x () String) (declare-fun y () String) (declare-fun z () String) (declare-fun w () String) (declare-fun w1 () String) (declare-fun w2 () String) (assert (= (str.++ x "aaaae") (str.++ "eaaaa" x))) (check-sat)