// Copyright rustc Contributors
// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/control-flow.rs
//
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// Modifications Copyright Kani Contributors
// See GitHub history for details.

// run-pass

// revisions: default nomiropt
//[nomiropt]compile-flags: -Z mir-opt-level=0

#![feature(generators, generator_trait)]

use std::marker::Unpin;
use std::ops::{Generator, GeneratorState};
use std::pin::Pin;

fn finish<T>(mut amt: usize, mut t: T) -> T::Return
where
    T: Generator<(), Yield = ()> + Unpin,
{
    loop {
        match Pin::new(&mut t).resume(()) {
            GeneratorState::Yielded(()) => amt = amt.checked_sub(1).unwrap(),
            GeneratorState::Complete(ret) => {
                assert_eq!(amt, 0);
                return ret;
            }
        }
    }
}

#[kani::proof]
#[kani::unwind(16)]
fn main() {
    finish(1, || yield);
    finish(8, || {
        for _ in 0..8 {
            yield;
        }
    });
    finish(1, || {
        if true {
            yield;
        } else {
        }
    });
    finish(1, || {
        if false {
        } else {
            yield;
        }
    });
    finish(2, || {
        if {
            yield;
            false
        } {
            yield;
            panic!()
        }
        yield
    });
}