diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 19:27:45 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 19:27:45 +0000 |
| commit | 9a994c449d65e64d574a423ad9caad519f8c2148 (patch) | |
| tree | 3c4571098d1771f8d277406c9f6e9c5b09dcd1da /test | |
| parent | 4bfa927dac67bbcadf219f70e61f1d123e33944b (diff) | |
merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/v1l20009.cvc | 4 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/wrong-sel-simp.cvc | 7 |
3 files changed, 11 insertions, 3 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 8785ae0db..f3ea1171d 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -36,7 +36,8 @@ TESTS = \ v2l40025.cvc \ v3l60006.cvc \ v5l30058.cvc \ - bug286.cvc + bug286.cvc \ + wrong-sel-simp.cvc FAILING_TESTS = rec5.cvc diff --git a/test/regress/regress0/datatypes/v1l20009.cvc b/test/regress/regress0/datatypes/v1l20009.cvc index 0adba1da7..64469cbd6 100644 --- a/test/regress/regress0/datatypes/v1l20009.cvc +++ b/test/regress/regress0/datatypes/v1l20009.cvc @@ -1,5 +1,5 @@ -% EXPECT: valid -% EXIT: 20 +% EXPECT: invalid +% EXIT: 10 DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc new file mode 100644 index 000000000..3ba3249f1 --- /dev/null +++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +DATATYPE + nat = succ(pred : nat) | zero +END; + +QUERY pred(zero) = zero; |