Attribute Macro unwind 

#[unwind]

Set Loop unwind limit for proof harnesses The attribute #[kani::unwind(arg)] can only be called alongside #[kani::proof]. arg - Takes in a integer value (u32) that represents the unwind value for the harness.