Skip to content

Commit 9611331

Browse files
committed
CI: Make smt2_solver available to all regression tests
We will want to use the solver for more than just selected CBMC regressions.
1 parent 062962c commit 9611331

File tree

1 file changed

+12
-5
lines changed

1 file changed

+12
-5
lines changed

.github/workflows/pull-request-checks.yaml

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -72,9 +72,10 @@ jobs:
7272
make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
7373
- name: Run regression tests
7474
run: |
75+
export PATH=$PATH:`pwd`/src/solvers
7576
make -C regression test-parallel JOBS=${{env.linux-vcpus}} LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
7677
make -C regression/cbmc test-paths-lifo
77-
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
78+
make -C regression/cbmc test-cprover-smt2
7879
make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
7980
- name: Check cleanup
8081
run: |
@@ -153,9 +154,10 @@ jobs:
153154
make TAGS="[!shouldfail]" -C jbmc/unit test
154155
- name: Run regression tests
155156
run: |
157+
export PATH=$PATH:`pwd`/src/solvers
156158
make -C regression test-parallel JOBS=${{env.linux-vcpus}}
157159
make -C regression/cbmc test-paths-lifo
158-
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
160+
make -C regression/cbmc test-cprover-smt2
159161
make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
160162
161163
# This job has been copied from the one above it, and modified to only build CBMC
@@ -339,9 +341,10 @@ jobs:
339341
make TAGS="[!shouldfail]" -C jbmc/unit test
340342
- name: Run regression tests
341343
run: |
344+
export PATH=$PATH:`pwd`/src/solvers
342345
make -C regression test-parallel JOBS=${{env.linux-vcpus}}
343346
make -C regression/cbmc test-paths-lifo
344-
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
347+
make -C regression/cbmc test-cprover-smt2
345348
make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
346349
347350
# This job takes approximately 17 to 41 minutes
@@ -689,7 +692,9 @@ jobs:
689692
- name: Run JBMC unit tests
690693
run: cd jbmc/unit; ./unit_tests
691694
- name: Run regression tests
692-
run: make -C regression test-parallel JOBS=4
695+
run: |
696+
export PATH=$PATH:`pwd`/src/solvers
697+
make -C regression test-parallel JOBS=4
693698
- name: Run JBMC regression tests
694699
run: make -C jbmc/regression test-parallel JOBS=4
695700

@@ -855,7 +860,9 @@ jobs:
855860
- name: Download minisat with make
856861
run: make -C src minisat2-download
857862
- name: Build CBMC with make
858-
run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
863+
run: |
864+
make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
865+
echo "$pwd\src\solvers;" >> $env:GITHUB_PATH
859866
- name: Build unit tests with make
860867
run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C unit all
861868
- name: Build jbmc with make

0 commit comments

Comments
 (0)