test/regress/regress2/sygus/qgu-bools.sy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

; COMMAND-LINE: --sygus-query-gen=unsat --sygus-abort-size=2
; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(query)'
; EXIT: 1
(set-logic ALL)
(synth-fun P ((a Bool) (b Bool) (c Bool)) Bool
((Start Bool))
(
(Start Bool (
a
b
c
(not Start)
(= Start Start)
(or Start Start)
(ite Start Start Start)
))
))


(check-synth)