Add CI job that runs KNOWNBUG tests

This is to make sure that we do not spuriously keep tests marked as
"KNOWNBUG" when a source change fixes the problem.

Author: tautschnig

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

@@ -457,3 +457,56 @@ jobs:
         run: make CXX=clcache BUILD_ENV=MSVC -j4 -C unit
       - name: Print ccache stats
         run: clcache -s
+
+  # This job takes approximately 2 minutes
+  check-ubuntu-24_04-make-gcc-KNOWNBUG:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq gcc gdb g++ jq flex bison libxml2-utils ccache cmake z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Prepare ccache
+        uses: actions/cache@v4
+        with:
+          path: .ccache
+          save-always: true
+          key: ${{ runner.os }}-24.04-make-gcc-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-24.04-make-gcc-${{ github.ref }}
+            ${{ runner.os }}-24.04-make-gcc
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Get cadical and minisat
+        run: make -C lib/cbmc/src cadical-download minisat2-download
+      - name: Build with make
+        run: make -C src -j4 CXX="ccache g++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
+      - name: Run the ebmc tests with SAT
+        run: make -C regression/ebmc test TEST_PL="../../lib/cbmc/regression/test.pl -K"
+      - name: Run the ebmc tests with Z3
+        run: make -C regression/ebmc test-z3 TEST_PL="../../lib/cbmc/regression/test.pl -K"
+      - name: Run the verilog tests
+        run: make -C regression/verilog test TEST_PL="../../lib/cbmc/regression/test.pl -K"
+      - name: Run the verilog tests with Z3
+        run: make -C regression/verilog test-z3 TEST_PL="../../lib/cbmc/regression/test.pl -K"
+      - name: Run the smv tests
+        run: make -C regression/smv test TEST_PL="../../lib/cbmc/regression/test.pl -K"
+      - name: Run the smv tests with Z3
+        run: make -C regression/smv test-z3 TEST_PL="../../lib/cbmc/regression/test.pl -K"
+      - name: Run the vlindex tests
+        run: make -C regression/vlindex test TEST_PL="../../lib/cbmc/regression/test.pl -K"
+      - name: Print ccache stats
+        run: ccache -s