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 ba4502b954f0f91c8b954130cd8702cbe7ac13f4..5fddcbd365a97a2ee746aa361536fe5980e5a0cb 100644 (file)
--- 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 }}