From f4ef742bc9ea5387d04bf51d1f539e78e7a2c08f Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 15 Mar 2024 22:32:57 -0700
Subject: [PATCH] Upgrade toolchain to nightly-2024-03-15

- Kani can no longer automatically detect loop bounds when using range.
---
 docs/src/getting-started/verification-results/src/main.rs | 1 +
 rust-toolchain.toml                                       | 2 +-
 tests/coverage/unreachable/abort/main.rs                  | 2 +-
 tests/expected/abort/main.rs                              | 1 +
 tests/expected/iterator/main.rs                           | 1 +
 tests/kani/Coroutines/main.rs                             | 1 +
 6 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/docs/src/getting-started/verification-results/src/main.rs b/docs/src/getting-started/verification-results/src/main.rs
index 7a03b34f0f9e..72653cf4dc8f 100644
--- a/docs/src/getting-started/verification-results/src/main.rs
+++ b/docs/src/getting-started/verification-results/src/main.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #[kani::proof]
+#[kani::unwind(4)]
 // ANCHOR: success_example
 fn success_example() {
     let mut sum = 0;
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 5b83049feef5..7035d1aba20f 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-03-14"
+channel = "nightly-2024-03-15"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/unreachable/abort/main.rs
index 2941ec126f3c..39c0b0efb54f 100644
--- a/tests/coverage/unreachable/abort/main.rs
+++ b/tests/coverage/unreachable/abort/main.rs
@@ -5,7 +5,7 @@
 
 use std::process;
 
-#[kani::proof]
+#[cfg_attr(kani, kani::proof, kani::unwind(5))]
 fn main() {
     for i in 0..4 {
         if i == 1 {
diff --git a/tests/expected/abort/main.rs b/tests/expected/abort/main.rs
index 2941ec126f3c..9e2f5b7a808c 100644
--- a/tests/expected/abort/main.rs
+++ b/tests/expected/abort/main.rs
@@ -6,6 +6,7 @@
 use std::process;
 
 #[kani::proof]
+#[kani::unwind(5)]
 fn main() {
     for i in 0..4 {
         if i == 1 {
diff --git a/tests/expected/iterator/main.rs b/tests/expected/iterator/main.rs
index b1cb4a89cfbf..5cf9402bcb23 100644
--- a/tests/expected/iterator/main.rs
+++ b/tests/expected/iterator/main.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #[kani::proof]
+#[kani::unwind(4)]
 fn main() {
     let mut z = 1;
     for i in 1..4 {
diff --git a/tests/kani/Coroutines/main.rs b/tests/kani/Coroutines/main.rs
index 10d92571aaa6..14cbeb426321 100644
--- a/tests/kani/Coroutines/main.rs
+++ b/tests/kani/Coroutines/main.rs
@@ -9,6 +9,7 @@ use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
+#[kani::unwind(3)]
 fn main() {
     let mut add_one = |mut resume: u8| {
         loop {