static mut WRAP_COUNTER: Option<u32> = None;

/// This function is safe and should never crash. Counter starts at 0.
#[kani::modifies(std::ptr::addr_of!(WRAP_COUNTER))]
#[kani::ensures(|_| true)]
pub fn next() -> u32 {
    // Safe in single-threaded.
    unsafe {
        match &WRAP_COUNTER {
            Some(val) => {
                WRAP_COUNTER = Some(val.wrapping_add(1));
                *val
            }
            None => {
                WRAP_COUNTER = Some(0);
                0
            }
        }
    }
}

#[kani::proof_for_contract(next)]
fn check_next() {
    let _ret = next();
}