Disable llbc feature by default

.github/workflows/kani.yml

@@ -70,6 +70,23 @@ jobs:
         env:
           RUST_TEST_THREADS: 1
 
+  llbc-regression:
+    runs-on: ubuntu-24.04
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v4
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: ubuntu-24.04
+
+      - name: Build Kani with Charon
+        run: cargo build-dev -- --features cprover --features llbc
+
+      - name: Run tests
+        run: ./scripts/kani-llbc-regression.sh
+
   documentation:
     runs-on: ubuntu-24.04
     permissions:

kani-compiler/Cargo.toml

@@ -31,7 +31,7 @@ tracing-tree = "0.4.0"
 
 # Future proofing: enable backend dependencies using feature.
 [features]
-default = ['cprover', 'llbc']
+default = ['cprover']
 llbc = ['charon']
 cprover = ['cbmc', 'num', 'serde']
 

scripts/kani-llbc-regression.sh

@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+if [[ -z $KANI_REGRESSION_KEEP_GOING ]]; then
+  set -o errexit
+fi
+set -o pipefail
+set -o nounset
+
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+export PATH=$SCRIPT_DIR:$PATH
+
+# Formatting check
+${SCRIPT_DIR}/kani-fmt.sh --check
+
+# Build kani
+cargo build-dev -- --features cprover --features llbc
+
+# Build compiletest and print configuration. We pick suite / mode combo so there's no test.
+echo "--- Compiletest configuration"
+cargo run -p compiletest --quiet -- --suite kani --mode cargo-kani --dry-run --verbose
+echo "-----------------------------"
+
+suite="llbc"
+mode="expected"
+echo "Check compiletest suite=$suite mode=$mode"
+cargo run -p compiletest --quiet -- --suite $suite --mode $mode \
+    --quiet --no-fail-fast
+
+echo
+echo "All Kani llbc regression tests completed successfully."
+echo