Run KNOWNBUG and THOROUGH regression tests in CI

Copy the check-ubuntu-20_04-cmake-gcc job to run KNOWNBUG (any test
reported as failure will tell us that a bug has unexpectedly been fixed)
an THOROUGH (tests that are expected to pass, but take longer to do so)
tests, each as a separate GitHub action.

Also run all tests tagged broken-smt-backend to confirm they haven't
been fixed.

Author: tautschnig

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

@@ -170,6 +170,90 @@ jobs:
       - name: Run tests
         run: cd build; ctest . -V -L CORE -j2
 
+  check-ubuntu-20_04-cmake-gcc-KNOWNBUG:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        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 cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
+      - name: Prepare ccache
+        uses: actions/cache@v2
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-20.04-Release-${{ github.ref }}
+            ${{ runner.os }}-20.04-Release
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -H. -Bbuild -G Ninja
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with Ninja
+        run: ninja -C build -j2
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run tests
+        run: |
+          cd build
+          ctest . -V -L KNOWNBUG -j2
+          export PATH=$PWD/bin:$PATH
+          cd ../regression/cbmc
+          sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc
+          # the following tests fail on Windows only
+          git checkout -- memory_allocation_1 printf1 union12 va_list3
+          # the following tests fail on Ubuntu 18.04 only
+          git checkout -- byte_update12 gcc_vector1
+          ../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K
+
+  check-ubuntu-20_04-cmake-gcc-THOROUGH:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        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 cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
+      - name: Prepare ccache
+        uses: actions/cache@v2
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-20.04-Release-${{ github.ref }}
+            ${{ runner.os }}-20.04-Release
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -H. -Bbuild -G Ninja
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with Ninja
+        run: ninja -C build -j2
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run tests
+        run: cd build; ctest . -V -L THOROUGH -j2
+
   check-macos-10_15-make-clang:
     runs-on: macos-10.15
     steps: