diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-09 05:25:31 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-09 05:25:31 +0000 |
| commit | 16ed35436d4e4914a2dc601947fcc9c184b264a7 (patch) | |
| tree | 2e98c5c78f32d3a6c93106cd4ad1a079c24dd2eb | |
| parent | 04fd25e4201130776015fd3179631a97f27da12a (diff) | |
one more simple test for uf
| -rw-r--r-- | test/regress/regress0/uf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/uf/Makefile.in | 3 | ||||
| -rw-r--r-- | test/regress/regress0/uf/simple.04.cvc | 11 |
3 files changed, 15 insertions, 2 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 3fcf179e9..fa298f1a5 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -1,7 +1,8 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4 TESTS = simple.01.cvc \ simple.02.cvc \ - simple.03.cvc + simple.03.cvc \ + simple.04.cvc # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress0/uf/Makefile.in b/test/regress/regress0/uf/Makefile.in index 22aeeff51..2707ec105 100644 --- a/test/regress/regress0/uf/Makefile.in +++ b/test/regress/regress0/uf/Makefile.in @@ -226,7 +226,8 @@ top_srcdir = @top_srcdir@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4 TESTS = simple.01.cvc \ simple.02.cvc \ - simple.03.cvc + simple.03.cvc \ + simple.04.cvc all: all-am diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc new file mode 100644 index 000000000..58bb6fef1 --- /dev/null +++ b/test/regress/regress0/uf/simple.04.cvc @@ -0,0 +1,11 @@ +% EXPECT: INVALID +A: TYPE; +B: TYPE; +x, y: A; +a, b: A; + +f: A -> B; + +ASSERT (x = a OR x = b) AND (y = b OR y = a); +QUERY (f(x) = f(y)); + |