test/regress/regress1/sygus/rand_p_0.sy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status
; EXPECT: unsat

(set-logic BV)
(set-option :sygus-active-gen-random-p 0)

; Ensures random enumerator correctly handles cases where the coin flips to
; tails but there is no no-argument constructor to pick.

(synth-fun f () Bool
  ((Start Bool) (Const Bool))
  ((Start Bool ((not Const)))
   (Const Bool (false))))

(check-synth)