Run benchcomp unit and regression tests in CI (model-checking#2382)

This will ensure that benchcomp will continue to correctly parse future changes to Kani's output.

.github/workflows/kani.yml

@@ -52,6 +52,29 @@ jobs:
           KANI_ENABLE_WRITE_JSON_SYMTAB: 1
         run: ./scripts/kani-regression.sh
 
+  benchcomp-tests:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v3
+
+      - name: Install benchcomp dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y python3-pip
+          pushd tools/benchcomp && pip3 install -r requirements.txt
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: ubuntu-20.04
+
+      - name: Build Kani using release mode
+        run: cargo build-dev -- --release
+
+      - name: Run benchcomp unit and regression tests
+        run: pushd tools/benchcomp && PATH=$(realpath ../../scripts):$PATH test/run
+
   perf:
     runs-on: ubuntu-20.04
     steps:

scripts/ci/copyright-exclude

@@ -5,8 +5,8 @@
 .png
 .props
 .public.key
-Cargo.lock
 CHANGELOG
+Cargo.lock
 LICENSE-APACHE
 LICENSE-MIT
 editorconfig
@@ -16,6 +16,7 @@ gitignore
 gitmodules
 ignore
 kani-dependencies
+requirements.txt
 scripts/ci/copyright-exclude
 tests/remote-target-lists/.*
 tools/build-kani/license-notes.txt

tools/benchcomp/requirements.txt

@@ -0,0 +1,2 @@
+cerberus
+pyyaml