diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-09-21 21:09:18 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-09-21 21:09:18 +0000 |
| commit | ba7aea0d9310015546bab5e5743c7dfcb0d2092d (patch) | |
| tree | 19ba631f0457b7946374c9a91a10121fe8839393 /test | |
| parent | b5e4b809d1913c9cfc5cf95c04e9fc34c1ca42f3 (diff) | |
Fixes for datatype dumping and printing. Add a new test case for dumping.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/datatype-dump.cvc | 20 |
2 files changed, 22 insertions, 1 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index de4f47bed..2ec558f20 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -44,7 +44,8 @@ TESTS = \ FAILING_TESTS = \ rec2.cvc \ - rec5.cvc + rec5.cvc \ + datatype-dump.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc b/test/regress/regress0/datatypes/datatype-dump.cvc new file mode 100644 index 000000000..44103eb1c --- /dev/null +++ b/test/regress/regress0/datatypes/datatype-dump.cvc @@ -0,0 +1,20 @@ +% This regression is the same as datatype.cvc but tests the +% dumping infrastructure. +% +% COMMAND-LINE: --dump assertions +% +% EXPECT: DATATYPE +% EXPECT: nat = succ(pred: nat) | zero +% EXPECT: END; +% EXPECT: x : nat; +% EXPECT: ASSERT NOT(NOT(is_succ(x)) AND NOT(is_zero(x))); +% EXPECT: CHECKSAT; +% EXPECT: invalid +% +% EXIT: 10 + +DATATYPE nat = succ(pred : nat) | zero END; + +x : nat; + +QUERY (NOT is_succ(x) AND NOT is_zero(x)); |