diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-06 09:24:11 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-06 09:24:11 -0600 |
| commit | 210e6db5c6a76ee1e554426058ecf3397575f1e3 (patch) | |
| tree | 98140a04acd9eedc91e2d598224ac7005d0a3540 /test/regress/regress2 | |
| parent | a727f6314c8f2ad72d8d83eb63c413bab68d1b08 (diff) | |
Support default sygus grammar construction for sets (#3842)
Fixes #3645.
Diffstat (limited to 'test/regress/regress2')
| -rw-r--r-- | test/regress/regress2/sygus/sets-fun-test.sy | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress2/sygus/sets-fun-test.sy b/test/regress/regress2/sygus/sets-fun-test.sy new file mode 100644 index 000000000..987d6a792 --- /dev/null +++ b/test/regress/regress2/sygus/sets-fun-test.sy @@ -0,0 +1,10 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) +(synth-fun f ((x Int)) (Set Int)) + +(constraint (member 45 (f 45))) +(constraint (member 8 (f 8))) +(constraint (member 0 (f 3))) + +(check-synth) |