From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 9 Mar 2010 05:25:31 +0000 (+0000)
Subject: one more simple test for uf
X-Git-Tag: cvc5-1.0.0~9195
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=16ed35436d4e4914a2dc601947fcc9c184b264a7;p=cvc5.git

one more simple test for uf
---

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));
+