From 706dbdac95131bf45efbfcb9a8ca4df9dfb85478 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 24 Aug 2020 11:54:18 -0700
Subject: [PATCH] Increase regress level to 2 for production build. (#4888)

---
 .github/workflows/ci.yml                                  | 6 +++++-
 test/regress/CMakeLists.txt                               | 8 ++++----
 .../{regress2 => regress3}/friedman_n4_i5.smtv1.smt2      | 0
 .../quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2      | 0
 .../{regress2 => regress3}/strings/norn-dis-0707-3.smt2   | 0
 .../{regress2 => regress3}/strings/replace_re_all.smt2    | 0
 6 files changed, 9 insertions(+), 5 deletions(-)
 rename test/regress/{regress2 => regress3}/friedman_n4_i5.smtv1.smt2 (100%)
 rename test/regress/{regress2 => regress3}/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2 (100%)
 rename test/regress/{regress2 => regress3}/strings/norn-dis-0707-3.smt2 (100%)
 rename test/regress/{regress2 => regress3}/strings/replace_re_all.smt2 (100%)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2d3586483..00fa15bc5 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -27,6 +27,7 @@ jobs:
             cache-key: production
             python-bindings: true
             check-examples: true
+            exclude_regress: 3-4
 
           - name: production-clang
             config: production
@@ -34,16 +35,19 @@ jobs:
             check-examples: true
             env: CC=clang CXX=clang++
             os: ubuntu-latest
+            exclude_regress: 1-4
 
           - name: debug
             config: debug --symfpu --lfsc --no-debug-symbols --editline
             cache-key: debug
             os: ubuntu-latest
+            exclude_regress: 1-4
 
           - name: debug-cln
             config: debug --symfpu --cln --gpl --no-debug-symbols --no-proofs
             cache-key: debug-cln
             os: ubuntu-latest
+            exclude_regress: 1-4
 
     name: ${{ matrix.os }}:${{ matrix.name }}
     runs-on: ${{ matrix.os }}
@@ -168,7 +172,7 @@ jobs:
     - name: Run CTest
       run: make -j2 check
       env:
-        ARGS: --output-on-failure -LE regress[1-4]
+        ARGS: --output-on-failure -LE regress[${{ matrix.exclude_regress }}]
         CVC4_REGRESSION_ARGS: --no-early-exit
       working-directory: build
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 99f06e0df..7a1366b3a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2080,7 +2080,6 @@ set(regress_2_tests
   regress2/bv_to_int_shifts.smt2
   regress2/error0.smt2
   regress2/error1.smtv1.smt2
-  regress2/friedman_n4_i5.smtv1.smt2
   regress2/fuzz_2.smtv1.smt2
   regress2/hash_sat_06_19.smt2
   regress2/hash_sat_07_17.smt2
@@ -2111,7 +2110,6 @@ set(regress_2_tests
   regress2/quantifiers/net-policy-no-time.smt2
   regress2/quantifiers/nunchaku2309663.nun.min.smt2
   regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
-  regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
   regress2/quantifiers/syn874-1.smt2
   regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
   regress2/strings/cmi-split-cm-fail.smt2
@@ -2122,12 +2120,10 @@ set(regress_2_tests
   regress2/strings/issue3203.smt2
   regress2/strings/issue918.smt2
   regress2/strings/non_termination_regular_expression6.smt2
-  regress2/strings/norn-dis-0707-3.smt2
   regress2/strings/range-perf.smt2
   regress2/strings/repl-repl-i-no-push.smt2
   regress2/strings/repl-repl.smt2
   regress2/strings/replace_re.smt2
-  regress2/strings/replace_re_all.smt2
   regress2/strings/replaceall-diffrange.smt2
   regress2/strings/replaceall-len-c.smt2
   regress2/strings/small-1.smt2
@@ -2165,6 +2161,10 @@ set(regress_2_tests
 # Regression level 3 tests
 
 set(regress_3_tests
+  regress3/strings/norn-dis-0707-3.smt2
+  regress3/strings/replace_re_all.smt2
+  regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
+  regress3/friedman_n4_i5.smtv1.smt2
   regress3/arith_prp-13-24.smt2
   regress3/bmc-ibm-1.smtv1.smt2
   regress3/bmc-ibm-2.smtv1.smt2
diff --git a/test/regress/regress2/friedman_n4_i5.smtv1.smt2 b/test/regress/regress3/friedman_n4_i5.smtv1.smt2
similarity index 100%
rename from test/regress/regress2/friedman_n4_i5.smtv1.smt2
rename to test/regress/regress3/friedman_n4_i5.smtv1.smt2
diff --git a/test/regress/regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2 b/test/regress/regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
similarity index 100%
rename from test/regress/regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
rename to test/regress/regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
diff --git a/test/regress/regress2/strings/norn-dis-0707-3.smt2 b/test/regress/regress3/strings/norn-dis-0707-3.smt2
similarity index 100%
rename from test/regress/regress2/strings/norn-dis-0707-3.smt2
rename to test/regress/regress3/strings/norn-dis-0707-3.smt2
diff --git a/test/regress/regress2/strings/replace_re_all.smt2 b/test/regress/regress3/strings/replace_re_all.smt2
similarity index 100%
rename from test/regress/regress2/strings/replace_re_all.smt2
rename to test/regress/regress3/strings/replace_re_all.smt2
-- 
2.30.2