diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-06 20:28:15 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-06 18:28:15 -0700 |
| commit | e4e3ac9d4dc62cad7f88f57bb0e80a3f2b32eecc (patch) | |
| tree | e53ce4f15a118b9bf482af8f3e6a448934d78413 /test/regress/regress1 | |
| parent | 79121aeeb03bf70323208d5059e23dfb62a83903 (diff) | |
Remove support for Enum sygus syntax. (#2264)
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/sygus/enum-test.sy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/enum-test.sy b/test/regress/regress1/sygus/enum-test.sy index 47099eeed..7364747fc 100644 --- a/test/regress/regress1/sygus/enum-test.sy +++ b/test/regress/regress1/sygus/enum-test.sy @@ -1,6 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) +;; this is the custom enumeration datatype syntax from an early proposal of the sygus standard (define-sort D (Enum (a b))) (define-fun f ((x D)) Int (ite (= x D::a) 3 7)) (synth-fun g () D ((Start D (D::a D::b)))) |