diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-10 15:50:56 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-10 15:51:08 -0500 |
| commit | 6ae07a91cdd4f20f8fdccd7e31d217c6ca34ee45 (patch) | |
| tree | 0f4f929831ba092b54a5919809a01f089e023b84 /test | |
| parent | 65128efc1d0a4c2007ebb7b47712888481c07843 (diff) | |
Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/datatype1.cvc | 2 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/datatype3.cvc | 2 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/wrong-sel-simp.cvc | 2 |
4 files changed, 5 insertions, 4 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 84adb4f84..e8a8f16f5 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -31,7 +31,6 @@ TESTS = \ datatype0.cvc \ datatype1.cvc \ datatype2.cvc \ - datatype3.cvc \ datatype4.cvc \ datatype13.cvc \ empty_tuprec.cvc \ @@ -64,6 +63,8 @@ TESTS = \ FAILING_TESTS = \ datatype-dump.cvc +# takes a long time to build model on debug : datatype3.cvc + EXTRA_DIST = $(TESTS) if CVC4_BUILD_PROFILE_COMPETITION diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc index 5172eeb48..3934959f1 100644 --- a/test/regress/regress0/datatypes/datatype1.cvc +++ b/test/regress/regress0/datatypes/datatype1.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc index 5f130b6ae..fff1a5dd7 100644 --- a/test/regress/regress0/datatypes/datatype3.cvc +++ b/test/regress/regress0/datatypes/datatype3.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc index 7455f809c..b0dbdc46e 100644 --- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc +++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE nat = succ(pred : nat) | zero END; |