// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// kani-flags: --default-unwind 2 --enable-unstable --cbmc-args --unwindset 2

#[kani::proof]
fn main() {}