diff options
Diffstat (limited to 'test/regress/regress1/sygus/enum-test.sy')
| -rw-r--r-- | test/regress/regress1/sygus/enum-test.sy | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/enum-test.sy b/test/regress/regress1/sygus/enum-test.sy new file mode 100644 index 000000000..47099eeed --- /dev/null +++ b/test/regress/regress1/sygus/enum-test.sy @@ -0,0 +1,8 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +(set-logic LIA) +(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)))) +(constraint (= (f g) 7)) +(check-synth) |