diff options
Diffstat (limited to 'test/regress/regress1/sygus/rand_p_0.sy')
-rw-r--r-- | test/regress/regress1/sygus/rand_p_0.sy | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/rand_p_0.sy b/test/regress/regress1/sygus/rand_p_0.sy new file mode 100644 index 000000000..a7b3c9f41 --- /dev/null +++ b/test/regress/regress1/sygus/rand_p_0.sy @@ -0,0 +1,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) |