blob: 2d911e56a4886bc4d04deea162846c3567930945 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
; EXIT: 1
(set-logic SLIA)
(synth-fun f ((x String) (y String)) Bool
((Start Bool) (StartRe RegLan) (StartStr String)) (
(Start Bool (
true
false
(= StartStr StartStr)
(str.in_re StartStr StartRe)
))
(StartRe RegLan (
re.allchar
(re.++ StartRe StartRe)
(re.union StartRe StartRe)
(re.* StartRe)
(str.to_re StartStr)
))
(StartStr String (
x y "A" "B" ""
(str.++ StartStr StartStr)
))
))
(check-synth)
|
