one more simple test for uf

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 3fcf179e9c67e6f217497661b5948ad31b7b0955..fa298f1a5efb272aecfe30907d0dc782e5110ce0 100644 (file)
--- 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 22aeeff510a891a19a480a4ebdd406bd8f682d9b..2707ec1058c7c695b312815aacb2e5caec2cd05a 100644 (file)
--- 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 (file)
index 0000000..58bb6fe
--- /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));
+