1 2 3 4 5 6 7 8 9 10 11 12 13 14
(set-logic QF_S) (set-info :status sat) (declare-fun x () String) (declare-fun y () String) (declare-fun z () String) ;plandowski p469 1 (assert (= (str.++ x "ab" y) (str.++ y "ba" z))) (assert (= z (str.++ x y))) (assert (not (= (str.++ x "a") (str.++ "a" x)))) (check-sat)