From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 16 Feb 2018 15:05:14 +0000 (-0800)
Subject: Make regress1 default, only test regress0 on Travis. (#1611)
X-Git-Tag: cvc5-1.0.0~5280
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ae2fb8ac9f22c9ad65a3d08dfe8319ea0160b0ea;p=cvc5.git

Make regress1 default, only test regress0 on Travis. (#1611)
---

diff --git a/.travis.yml b/.travis.yml
index 562987f3c..e8c858d18 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -81,7 +81,9 @@ script:
        error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED";
    }
    makeCheck() {
-     make V=1 -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/TEST FAILED";
+     make V=1 -j2 units || error "BUILD/UNIT TEST FAILED";
+     make V=1 -j2 systemtests || error "BUILD/SYSTEM TEST FAILED";
+     make V=1 -j2 regress0 CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/REGRESSION TEST FAILED";
    }
    makeExamples() {
      make V=1 -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}";
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index b9864d51b..0c2c8a565 100644
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = regress0
+SUBDIRS = regress0 regress1
 DIST_SUBDIRS = regress0 regress1 regress2 regress3 regress4
 
 @mk_include@ @srcdir@/Makefile.levels