blob: 955245f87a1ec461515a32b3502d461bf484a589 (
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
34
35
36
37
38
39
40
41
|
; COMMAND-LINE: --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 BV)
(synth-fun f ( (x Bool) (y Bool) (z Bool) (w Bool) ) Bool
((Start Bool (
(and depth1 depth1)
(not depth1)
(or depth1 depth1)
(xor depth1 depth1)
))
(depth1 Bool (
(and depth2 depth2)
(not depth2)
(or depth2 depth2)
(xor depth2 depth2)
x
))
(depth2 Bool (
(and depth3 depth3)
(not depth3)
(or depth3 depth3)
(xor depth3 depth3)
w
))
(depth3 Bool (
(and depth4 depth4)
(not depth4)
(or depth4 depth4)
(xor depth4 depth4)
y
))
(depth4 Bool (
z
)))
)
(check-synth)
|
