1 2 3 4 5 6 7 8 9 10 11 12
; COMMAND-LINE: --strings-exp ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) (declare-fun x () String) (declare-fun y () String) (declare-fun z () String) (declare-fun w () String) (assert (= x (str.rev (str.++ y "A")))) (assert (= x (str.rev (str.++ "B" z)))) (assert (= z (str.++ w "C"))) (check-sat)