diff --git a/docs/src/getting-started/verification-results/src/main.rs b/docs/src/getting-started/verification-results/src/main.rs index 72653cf4dc8f..7a03b34f0f9e 100644 --- a/docs/src/getting-started/verification-results/src/main.rs +++ b/docs/src/getting-started/verification-results/src/main.rs @@ -2,7 +2,6 @@ // 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/tests/coverage/unreachable/abort/main.rs b/tests/coverage/unreachable/abort/main.rs index 39c0b0efb54f..2941ec126f3c 100644 --- a/tests/coverage/unreachable/abort/main.rs +++ b/tests/coverage/unreachable/abort/main.rs @@ -5,7 +5,7 @@ use std::process; -#[cfg_attr(kani, kani::proof, kani::unwind(5))] +#[kani::proof] 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 9e2f5b7a808c..2941ec126f3c 100644 --- a/tests/expected/abort/main.rs +++ b/tests/expected/abort/main.rs @@ -6,7 +6,6 @@ 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 5cf9402bcb23..b1cb4a89cfbf 100644 --- a/tests/expected/iterator/main.rs +++ b/tests/expected/iterator/main.rs @@ -2,7 +2,6 @@ // 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 e059305a6da2..0742d14a6ada 100644 --- a/tests/kani/Coroutines/main.rs +++ b/tests/kani/Coroutines/main.rs @@ -10,7 +10,6 @@ use std::ops::{Coroutine, CoroutineState}; use std::pin::Pin; #[kani::proof] -#[kani::unwind(3)] fn main() { let mut add_one = #[coroutine] |mut resume: u8| {