diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
-rw-r--r-- | test/regress/regress1/sygus/rand_const.sy | 12 | ||||
-rw-r--r-- | test/regress/regress1/sygus/rand_p_0.sy | 15 | ||||
-rw-r--r-- | test/regress/regress1/sygus/rand_p_1.sy | 14 |
4 files changed, 44 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 20722a1da..ffff25520 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2531,6 +2531,9 @@ set(regress_1_tests regress1/sygus/pLTL_5_trace.sy regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 + regress1/sygus/rand_const.sy + regress1/sygus/rand_p_0.sy + regress1/sygus/rand_p_1.sy regress1/sygus/real-any-const.sy regress1/sygus/real-grammar.sy regress1/sygus/rec-fun-swap.sy diff --git a/test/regress/regress1/sygus/rand_const.sy b/test/regress/regress1/sygus/rand_const.sy new file mode 100644 index 000000000..e920a9cc0 --- /dev/null +++ b/test/regress/regress1/sygus/rand_const.sy @@ -0,0 +1,12 @@ +; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status +; EXPECT: unsat + +(set-logic BV) + +; Ensures random enumerator correctly handles non-sygus types. + +(synth-fun f () (_ BitVec 7) + ((Start (_ BitVec 7))) + ((Start (_ BitVec 7) ((Constant (_ BitVec 7)))))) + +(check-synth) 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) 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) |