1 2 3 4 5 6 7 8 9 10 11 12 13 14
; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status (set-logic SLIA) (synth-fun f ((name String)) String ((Start String (name "A" "B" (str.++ Start Start))))) (declare-var name String) (constraint (= (f "BB") "AAAAAAAAAAAABAAAAAAAABAAA")) (check-synth)