summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uf
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/uf')
-rw-r--r--test/regress/regress0/uf/Makefile.am2
-rw-r--r--test/regress/regress0/uf/simple.01.cvc1
-rw-r--r--test/regress/regress0/uf/simple.02.cvc1
-rw-r--r--test/regress/regress0/uf/simple.03.cvc1
-rw-r--r--test/regress/regress0/uf/simple.04.cvc1
5 files changed, 5 insertions, 1 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index ec99fd45c..802189f2b 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
TESTS = \
euf_simp01.smt \
euf_simp02.smt \
diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc
index f5d8c1033..84b8b8a8d 100644
--- a/test/regress/regress0/uf/simple.01.cvc
+++ b/test/regress/regress0/uf/simple.01.cvc
@@ -5,3 +5,4 @@ x, y: A;
f: A -> B;
QUERY (x = y => f(x) = f(y));
+% EXIT: 20
diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc
index 0ebc319ba..21d3e3cee 100644
--- a/test/regress/regress0/uf/simple.02.cvc
+++ b/test/regress/regress0/uf/simple.02.cvc
@@ -5,3 +5,4 @@ x, y: A;
f: A -> B;
QUERY (f(x) = f(y));
+% EXIT: 10
diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc
index 54948edb8..476c6cd4a 100644
--- a/test/regress/regress0/uf/simple.03.cvc
+++ b/test/regress/regress0/uf/simple.03.cvc
@@ -9,3 +9,4 @@ f: A -> B;
ASSERT (x = a AND y = a) OR (x = b AND y = b);
QUERY (f(x) = f(y));
+% EXIT: 20
diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc
index 58bb6fef1..c9675588d 100644
--- a/test/regress/regress0/uf/simple.04.cvc
+++ b/test/regress/regress0/uf/simple.04.cvc
@@ -9,3 +9,4 @@ f: A -> B;
ASSERT (x = a OR x = b) AND (y = b OR y = a);
QUERY (f(x) = f(y));
+% EXIT: 10
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback