1 2 3 4 5 6 7 8
; EXPECT: sat (set-logic ALL) (set-option :incremental false) (declare-fun x () String) (declare-fun y () String) (assert (= (str.++ (str.rev "abc") "d") x)) (assert (= (str.++ (str.tolower "ABC") (str.toupper "abc")) y)) (check-sat)