From 16ed35436d4e4914a2dc601947fcc9c184b264a7 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Tue, 9 Mar 2010 05:25:31 +0000 Subject: one more simple test for uf --- test/regress/regress0/uf/Makefile.am | 3 ++- test/regress/regress0/uf/Makefile.in | 3 ++- test/regress/regress0/uf/simple.04.cvc | 11 +++++++++++ 3 files changed, 15 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/uf/simple.04.cvc (limited to 'test') 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)); + -- cgit v1.2.3