|
72 | 72 | make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss |
73 | 73 | - name: Run regression tests |
74 | 74 | run: | |
| 75 | + export PATH=$PATH:`pwd`/src/solvers |
75 | 76 | make -C regression test-parallel JOBS=${{env.linux-vcpus}} LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss |
76 | 77 | 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 |
78 | 79 | make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} |
79 | 80 | - name: Check cleanup |
80 | 81 | run: | |
@@ -153,9 +154,10 @@ jobs: |
153 | 154 | make TAGS="[!shouldfail]" -C jbmc/unit test |
154 | 155 | - name: Run regression tests |
155 | 156 | run: | |
| 157 | + export PATH=$PATH:`pwd`/src/solvers |
156 | 158 | make -C regression test-parallel JOBS=${{env.linux-vcpus}} |
157 | 159 | 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 |
159 | 161 | make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} |
160 | 162 |
|
161 | 163 | # This job has been copied from the one above it, and modified to only build CBMC |
@@ -339,9 +341,10 @@ jobs: |
339 | 341 | make TAGS="[!shouldfail]" -C jbmc/unit test |
340 | 342 | - name: Run regression tests |
341 | 343 | run: | |
| 344 | + export PATH=$PATH:`pwd`/src/solvers |
342 | 345 | make -C regression test-parallel JOBS=${{env.linux-vcpus}} |
343 | 346 | 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 |
345 | 348 | make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} |
346 | 349 |
|
347 | 350 | # This job takes approximately 17 to 41 minutes |
@@ -689,7 +692,9 @@ jobs: |
689 | 692 | - name: Run JBMC unit tests |
690 | 693 | run: cd jbmc/unit; ./unit_tests |
691 | 694 | - 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 |
693 | 698 | - name: Run JBMC regression tests |
694 | 699 | run: make -C jbmc/regression test-parallel JOBS=4 |
695 | 700 |
|
|
0 commit comments