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