Skip to content

Commit 7cb9ed2

Browse files
committed
Use 4 vCPUs for running coverage-recording tests
We changed the number of vCPUs for most scenarios in 55e5bdf, but failed to also propagate this to coverage-recording test execution.
1 parent 3e5e423 commit 7cb9ed2

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

.github/workflows/coverage.yaml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ env:
1010
windows-vcpus: 4
1111

1212
jobs:
13-
# This job takes approximately 40 to 75 minutes
13+
# This job takes approximately 22 to 75 minutes
1414
Linux:
1515
runs-on: ubuntu-20.04
1616
steps:
@@ -54,7 +54,7 @@ jobs:
5454
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
5555
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
5656
- name: Configure CMake CBMC build with coverage instrumentation parameters
57-
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=2 -DCMAKE_CXX_COMPILER=/usr/bin/g++
57+
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=${{env.linux-vcpus}} -DCMAKE_CXX_COMPILER=/usr/bin/g++
5858
- name: Zero ccache stats and limit in size
5959
run: ccache -z --max-size=7G
6060
- name: Execute CMake CBMC build

0 commit comments

Comments
 (0)