diff options
Diffstat (limited to 'test/regress/regress1/sygus/rand_p_1.sy')
-rw-r--r-- | test/regress/regress1/sygus/rand_p_1.sy | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/rand_p_1.sy b/test/regress/regress1/sygus/rand_p_1.sy new file mode 100644 index 000000000..412e55f73 --- /dev/null +++ b/test/regress/regress1/sygus/rand_p_1.sy @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status +; EXPECT: unsat + +(set-logic BV) +(set-option :sygus-active-gen-random-p 1) + +; Ensures random enumerator correctly handles cases where the coin flips to +; heads but there is no constructor that takes arguments to pick. + +(synth-fun f () Bool + ((Start Bool)) + ((Start Bool (false)))) + +(check-synth) |