Remove unneeded unwinds from unbounded benchmarks (#2431)

Author: qinheping

tests/kani/AsyncAwait/main.rs

@@ -14,23 +14,20 @@ use std::{
 fn main() {}
 
 #[kani::proof]
-#[kani::unwind(2)]
 async fn test_async_proof_harness() {
     let async_block_result = async { 42 }.await;
     let async_fn_result = async_fn().await;
     assert_eq!(async_block_result, async_fn_result);
 }
 
 #[kani::proof]
-#[kani::unwind(2)]
 pub async fn test_async_proof_harness_pub() {
     let async_block_result = async { 42 }.await;
     let async_fn_result = async_fn().await;
     assert_eq!(async_block_result, async_fn_result);
 }
 
 #[kani::proof]
-#[kani::unwind(2)]
 fn test_async_await() {
     // Test using the `block_on` implementation in Kani's library
     kani::block_on(async {

tests/kani/Drop/drop_after_moving_across_channel.rs

@@ -18,7 +18,6 @@ impl Drop for DropSetCELLToOne {
     }
 }
 
-#[kani::unwind(1)]
 #[kani::proof]
 fn main() {
     {

tests/kani/Generator/rustc-generator-tests/conditional-drop.rs

@@ -35,7 +35,6 @@ fn test2() -> bool {
 }
 
 #[kani::proof]
-#[kani::unwind(4)]
 fn main() {
     t1();
     t2();

tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs

@@ -14,7 +14,6 @@ use std::ops::Generator;
 use std::pin::Pin;
 
 #[kani::proof]
-#[kani::unwind(2)]
 fn main() {
     let b = |_| 3;
     let mut a = || {

tests/kani/Generator/rustc-generator-tests/moved-locals.rs

@@ -79,7 +79,6 @@ fn overlap_x_and_y() -> impl Generator<Yield = (), Return = ()> {
 }
 
 #[kani::proof]
-#[kani::unwind(129)]
 fn main() {
     let mut generator = move_before_yield();
     assert_eq!(

tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs

@@ -20,7 +20,6 @@ use std::mem::size_of_val;
 fn take<T>(_: T) {}
 
 #[kani::proof]
-#[kani::unwind(2)]
 fn main() {
     let x = false;
     let mut gen1 = || {

tests/kani/Generator/rustc-generator-tests/static-generator.rs

@@ -14,7 +14,6 @@ use std::ops::{Generator, GeneratorState};
 use std::pin::Pin;
 
 #[kani::proof]
-#[kani::unwind(2)]
 fn main() {
     let mut generator = static || {
         let a = true;

tests/kani/Generator/rustc-generator-tests/yield-in-box.rs

@@ -15,7 +15,6 @@ use std::ops::GeneratorState;
 use std::pin::Pin;
 
 #[kani::proof]
-#[kani::unwind(2)]
 fn main() {
     let x = 0i32;
     || {

tests/kani/PointerComparison/ptr_comparison.rs

@@ -102,7 +102,6 @@ fn check_slice_len() {
 
 // Check comparison of box.
 #[cfg_attr(kani, kani::proof)]
-#[cfg_attr(kani, kani::unwind(4))]
 fn check_box_comparison() {
     let obj = Box::new([0u16, 10]);
     let first: *const [u16] = &obj[1..2];