; 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 BV)

(synth-fun f ( (x Bool) (y Bool) (z Bool) (w Bool) ) Bool
 ( (Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 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)