Merge branch 'main' into issue-3612-can-deref-2

Author: celinval

.github/workflows/kani.yml

@@ -31,27 +31,6 @@ jobs:
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
-  write-json-symtab-regression:
-    runs-on: ubuntu-20.04
-    steps:
-      - name: Checkout Kani
-        uses: actions/checkout@v4
-
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-20.04
-
-      - name: Build Kani
-        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
-
-
   benchcomp-tests:
     runs-on: ubuntu-20.04
     steps:

.github/workflows/release.yml

@@ -272,7 +272,7 @@ jobs:
       - name: Run tests
         # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests.
         run: |
-          for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
+          for dir in simple-lib build-rs-works simple-kissat; do
             >&2 echo "Running test $dir"
             pushd tests/cargo-kani/$dir
             cargo kani
@@ -312,7 +312,7 @@ jobs:
 
       - name: Run installed tests
         run: |
-          for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
+          for dir in simple-lib build-rs-works simple-kissat; do
             >&2 echo "Running test $dir"
             docker run -v /var/run/docker.sock:/var/run/docker.sock \
               -w /tmp/kani/tests/cargo-kani/$dir kani-18-04 cargo kani

.github/workflows/verify-std-check.yml

@@ -59,7 +59,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates
+            -Z mem-predicates -Z loop-contracts --enable-unstable --cbmc-args --object-bits 12
 
       # If the head failed, check if it's a new failure.
       - name: Checkout base
@@ -77,7 +77,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates
+            -Z mem-predicates -Z loop-contracts --enable-unstable --cbmc-args --object-bits 12
 
       - name: Compare PR results
         if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome