diff options
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)); |