1 2 3 4 5 6 7 8 9 10 11 12 13 14
; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status (set-logic ALL) (synth-fun f ((x String) (y String)) String) (synth-fun g ((x String) (y String)) String) (declare-var x String) (declare-var y String) (constraint (= (f x y) (str.replace (str.++ x y) "A" "ABCD"))) (constraint (= (g x y) (str.replace (f x y) "B" "CDE"))) (check-synth)