From: Gereon Kremer <nafur42@gmail.com>
Date: Sat, 6 Nov 2021 01:05:58 +0000 (-0700)
Subject: Only run regress0 for static build (#7592)
X-Git-Tag: cvc5-1.0.0~871
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=733ab2f6b9430b2ae5824e2614de5811a60033f3;p=cvc5.git

Only run regress0 for static build (#7592)

It is surprisingly tricky to call ctest properly with multiple -LE arguments (and I actually doubt that the CI version of ctest adheres to its documentation). This PR avoid calling make check (which sets -LE regress[3-4] as a default) and calls ctest directly.
---

diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml
index ba4502b95..5fddcbd36 100644
--- a/.github/actions/run-tests/action.yml
+++ b/.github/actions/run-tests/action.yml
@@ -21,9 +21,9 @@ runs:
     - name: Run CTest
       shell: bash
       run: |
-        make -j${{ env.num_proc }} check
+        make -j${{ env.num_proc }} build-tests
+        ctest -j${{ env.num_proc }} --output-on-failure -LE regress[${{ inputs.regressions-exclude }}]
       env:
-        ARGS: --output-on-failure -LE regress[${{ inputs.regressions-exclude }}]
         CVC5_REGRESSION_ARGS: --no-early-exit
         RUN_REGRESSION_ARGS: ${{ inputs.regressions-args }}
       working-directory: ${{ inputs.build-dir }}