From 1363708339aa4d959b65b27f3e032f4dc1c7b83c Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 15 May 2023 20:23:03 -0700
Subject: [PATCH 1/2] Cleanup the symtab json in case we ever use that

This should also fix the out of space error from the symtab json
regression
---
 kani-driver/src/project.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
index adf88c1ba580..c776a106ae47 100644
--- a/kani-driver/src/project.rs
+++ b/kani-driver/src/project.rs
@@ -129,12 +129,12 @@ impl Project {
                 let goto = Artifact::try_new(&goto_path, Goto)?;
 
                 // All other harness artifacts that may have been generated as part of the build.
-                artifacts.extend([TypeMap, VTableRestriction, PrettyNameMap].iter().filter_map(
-                    |typ| {
+                artifacts.extend(
+                    [SymTab, TypeMap, VTableRestriction, PrettyNameMap].iter().filter_map(|typ| {
                         let artifact = Artifact::try_from(&symtab_out, *typ).ok()?;
                         Some(artifact)
-                    },
-                ));
+                    }),
+                );
                 artifacts.push(symtab_out);
                 artifacts.push(goto);
             }

From 8a35c7b71d722e28084638669b6153b5e8aad052 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 16 May 2023 14:53:20 -0700
Subject: [PATCH 2/2] Only run a few set of tests

---
 .github/workflows/kani.yml | 12 +++++++-----
 scripts/kani-regression.sh | 13 +++----------
 2 files changed, 10 insertions(+), 15 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 0fe56706140f..eac9372905cc 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -45,12 +45,14 @@ jobs:
           os: ubuntu-20.04
 
       - name: Build Kani
-        run: cargo build-dev
+        run: cargo build-dev -- --features write_json_symtab
+
+      - name: Run tests
+        run: |
+          cargo run -p compiletest --quiet -- --suite kani --mode kani --quiet --no-fail-fast
+          cargo run -p compiletest --quiet -- --suite expected --mode expected --quiet --no-fail-fast
+          cargo run -p compiletest --quiet -- --suite cargo-kani --mode cargo-kani --quiet --no-fail-fast
 
-      - name: Execute Kani regression
-        env:
-          KANI_ENABLE_WRITE_JSON_SYMTAB: 1
-        run: ./scripts/kani-regression.sh
 
   benchcomp-tests:
     runs-on: ubuntu-20.04
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index 8dfd8b53ce53..4a92426f6019 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -27,11 +27,7 @@ check_kissat_version.sh
 ${SCRIPT_DIR}/kani-fmt.sh --check
 
 # Build all packages in the workspace
-if [[ "" != "${KANI_ENABLE_WRITE_JSON_SYMTAB-}" ]]; then
-  cargo build-dev -- --features write_json_symtab
-else
-  cargo build-dev
-fi
+cargo build-dev
 
 # Unit tests
 cargo test -p cprover_bindings
@@ -69,11 +65,8 @@ for testp in "${TESTS[@]}"; do
       --quiet --no-fail-fast
 done
 
-# Don't run std regression if using JSON symtab to avoid OOM issues.
-if [[ -z "${KANI_ENABLE_WRITE_JSON_SYMTAB-}" ]]; then
-    # Check codegen for the standard library
-    time "$SCRIPT_DIR"/std-lib-regression.sh
-fi
+# Check codegen for the standard library
+time "$SCRIPT_DIR"/std-lib-regression.sh
 
 # We rarely benefit from re-using build artifacts in the firecracker test,
 # and we often end up with incompatible leftover artifacts: