; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)

(synth-fun f ((x String) (y String)) String)

(declare-var x String)
(declare-var y String)

(constraint (= (f x y) (str.replace (str.++ x y) "A" "ABCD")))

(check-synth)