test/regress/regress1/sygus/re-concat.sy


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)