diff options
-rw-r--r-- | .github/workflows/ci.yml | 6 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 8 | ||||
-rw-r--r-- | test/regress/regress3/friedman_n4_i5.smtv1.smt2 (renamed from test/regress/regress2/friedman_n4_i5.smtv1.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2 (renamed from test/regress/regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress3/strings/norn-dis-0707-3.smt2 (renamed from test/regress/regress2/strings/norn-dis-0707-3.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress3/strings/replace_re_all.smt2 (renamed from test/regress/regress2/strings/replace_re_all.smt2) | 0 |
6 files changed, 9 insertions, 5 deletions
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 index 604aa2dfb..604aa2dfb 100644 --- a/test/regress/regress2/friedman_n4_i5.smtv1.smt2 +++ b/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 index 23b4c8cbd..23b4c8cbd 100644 --- a/test/regress/regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2 +++ b/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 index 242d7e958..242d7e958 100644 --- a/test/regress/regress2/strings/norn-dis-0707-3.smt2 +++ b/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 index cf2b674c3..cf2b674c3 100644 --- a/test/regress/regress2/strings/replace_re_all.smt2 +++ b/test/regress/regress3/strings/replace_re_all.smt2 |