From 9a994c449d65e64d574a423ad9caad519f8c2148 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 27 Jul 2012 19:27:45 +0000 Subject: 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 --- test/regress/regress0/datatypes/Makefile.am | 3 ++- test/regress/regress0/datatypes/v1l20009.cvc | 4 ++-- test/regress/regress0/datatypes/wrong-sel-simp.cvc | 7 +++++++ 3 files changed, 11 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/datatypes/wrong-sel-simp.cvc (limited to 'test/regress') 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; -- cgit v1.2.3