Downgrade the toolchain to avoid blocking issue

Mitigates model-checking#1822 which is
caused by rust-lang/rust#103814.

Ps.: I also bumped cbmc min version since older versions don't work with
Kani.

Author: celinval

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2022-10-25"
-components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
+channel = "nightly-2022-10-24"
+components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

scripts/kani-regression.sh

@@ -22,7 +22,7 @@ KANI_DIR=$SCRIPT_DIR/..
 export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true"
 
 # Required dependencies
-check-cbmc-version.py --major 5 --minor 67
+check-cbmc-version.py --major 5 --minor 69
 check-cbmc-viewer-version.py --major 3 --minor 5
 
 # Formatting check
@@ -60,7 +60,7 @@ TESTS=(
 
 if [[ "" != "${KANI_ENABLE_UNSOUND_EXPERIMENTS-}" ]]; then
   TESTS+=("unsound_experiments kani")
-else 
+else
   TESTS+=("no_unsound_experiments expected")
 fi
 

tests/kani/ConstEval/limit.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Ensure that constant propagation can deal with a large number.
+// This test used to trigger https://github.com/rust-lang/rust/issues/103814
+
+const LENGTH: usize = 131072;
+const CONST: usize = {
+    let data = [1; LENGTH];
+    let mut idx = 0;
+    while idx < data.len() {
+        idx += data[idx];
+    }
+    idx
+};
+
+#[kani::proof]
+fn check_eval() {
+    assert_eq!(CONST, LENGTH);
+}