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

   1 ; COMMAND-LINE: --sygus-query-gen=unsat --sygus-abort-size=2
   2 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
   3 ; SCRUBBER: grep -v -E '(\(define-fun|\(query)'
   4 ; EXIT: 1
   5 (set-logic ALL)
   6 (synth-fun P ((a Bool) (b Bool) (c Bool)) Bool
   7 ((Start Bool))
   8 (
   9 (Start Bool (
  10 a
  11 b
  12 c
  13 (not Start)
  14 (= Start Start)
  15 (or Start Start)
  16 (ite Start Start Start)
  17 ))
  18 ))
  19
  20
  21 (check-synth)