1 2 3 4 5 6 7 8 9 10 11 12 13 14
; COMMAND-LINE: --strings-exp ; EXPECT: unsat (set-logic QF_SLIA) (set-info :status unsat) (declare-fun x () String) (declare-fun y () String) (declare-fun z () String) (declare-fun w () String) (assert (str.<= x y)) (assert (str.<= y w)) (declare-fun xp () String) (assert (= x (str.++ "G" xp))) (assert (= w "E")) (check-sat)