* added test/regress/regress0/arith for easy arithmetic regress tests.

diff --git a/test/Makefile.am b/test/Makefile.am
index 045599bc11c5b2c9cb5211762f7b092f19df8ef8..a257b96d9308e093d10dc77d2af346106fc22a94 100644 (file)
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \
   blu='\e[1;34m'; \
   std='\e[m'; \
 }
-subdirs_to_check = unit system regress/regress0 regress/regress0/uf regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
+subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
 check-recursive: check-pre
 .PHONY: check-pre
 check-pre:

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 7f732b17fdee43e1926883413bb193465ab42e22..c376be91b6bd3c6f4b7932546880ea6e4671b2ea 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . precedence uf
+SUBDIRS = . arith precedence uf
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
new file mode 100644 (file)
index 0000000..e4fc110
--- /dev/null
+++ b/test/regress/regress0/arith/Makefile.am
@@ -0,0 +1,28 @@
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =        \
+       arith.01.cvc \
+       arith.02.cvc 
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#      error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#      error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:

diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc
new file mode 100644 (file)
index 0000000..5b4a33b
--- /dev/null
+++ b/test/regress/regress0/arith/arith.01.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+x : REAL;
+y : REAL;
+
+QUERY (x * y ) = (y * x);
+% EXIT: 20

diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc
new file mode 100644 (file)
index 0000000..a2c93da
--- /dev/null
+++ b/test/regress/regress0/arith/arith.02.cvc
@@ -0,0 +1,7 @@
+% EXPECT: VALID
+x : REAL;
+y : REAL;
+z : REAL;
+
+QUERY x*(y*z) = (x*y)*z;
+% EXIT: 20

diff --git a/test/regress/regress0/arith/arith.03.cvc b/test/regress/regress0/arith/arith.03.cvc
new file mode 100644 (file)
index 0000000..96af458
--- /dev/null
+++ b/test/regress/regress0/arith/arith.03.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+x : REAL;
+y : REAL;
+
+QUERY (x + y)*(x + y) = x*x + 2*x*y + y*y;
+% EXIT: 20