Adding tests for precedence of arithmetic in CVC inputs

1 files changed, 30 insertions, 17 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 830b1022d..8eb745637 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -5,11 +5,16 @@ 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 =	\
-	boolean-prec.cvc \
+
+# Regression tests for SMT inputs
+SMT_TESTS = \
 	distinct.smt \
 	flet.smt \
 	flet2.smt \
+	fuzz_1.smt \
+	fuzz_3.smt \
+	ineq_basic.smt \
+	ineq_slack.smt \
 	ite_real_int_type.smt \
 	ite_real_valid.smt \
 	let.smt \
@@ -18,21 +23,21 @@ TESTS =	\
 	simple2.smt \
         simple-lra.smt \
         simple-rdl.smt \
-	simple-uf.smt \
-	ite.smt2 \
+	simple-uf.smt
+
+# Regression tests for SMT2 inputs
+SMT2_TESTS = \
 	ite2.smt2 \
 	ite3.smt2 \
 	ite4.smt2 \
         simple-lra.smt2 \
         simple-rdl.smt2 \
-	simple-uf.smt2 \
-	bug2.smt \
-	bug32.cvc \
-	bug49.smt \
-	bug161.smt \
-	bug164.smt \
-	bug167.smt \
-	bug168.smt \
+	simple-uf.smt2
+
+# Regression tests for PL inputs
+CVC_TESTS = \
+	boolean-prec.cvc \
+        ite.cvc \
 	hole6.cvc \
 	logops.01.cvc \
 	logops.02.cvc \
@@ -40,8 +45,6 @@ TESTS =	\
 	logops.04.cvc \
 	logops.05.cvc \
 	simple.cvc \
-	ineq_basic.smt \
-	ineq_slack.smt \
 	smallcnf.cvc \
 	test11.cvc \
 	test9.cvc \
@@ -66,9 +69,19 @@ TESTS =	\
 	wiki.18.cvc \
 	wiki.19.cvc \
 	wiki.20.cvc \
-	wiki.21.cvc \
-	fuzz_1.smt \
-	fuzz_3.smt
+	wiki.21.cvc
+
+# Regression tests derived from bug reports
+BUG_TESTS = \
+	bug2.smt \
+	bug32.cvc \
+	bug49.smt \
+	bug161.smt \
+	bug164.smt \
+	bug167.smt \
+	bug168.smt
+
+TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS)