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 {