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


1
2
3
4
5
6
7
8
9
10
11
12
13

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic SLIA)
(synth-fun f () RegLan (
                         (Start RegLan (
                                         (str.to.re Tokens)
                                         (re.++ Start Start)))
                         (Tokens String ("A" "B"))
                         ))

(constraint (str.in.re "AB" f))

(check-synth)