1 2 3 4 5 6 7 8 9 10 11 12 13
; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) (synth-fun f () RegLan ((Start RegLan) (Tokens String)) ( (Start RegLan ( (str.to_re Tokens) (re.++ Start Start))) (Tokens String ("A" "B")) )) (constraint (str.in_re "AB" f)) (check-synth)