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

//! This test is to check how Kani handle enums where only one variant is valid.
#![feature(never_type)]

enum MyResult<Y, N, M> {
    Yes(Y),
    No(N),
    Maybe(M),
}

fn change_maybe<Y, N, M, O>(orig: MyResult<Y, N, M>, val: O) -> MyResult<Y, N, O> {
    match orig {
        MyResult::Yes(y) => MyResult::Yes(y),
        MyResult::No(n) => MyResult::No(n),
        MyResult::Maybe(m) => MyResult::Maybe(val),
    }
}

fn check() -> Result<u32, !> {
    let val = Result::<u32, !>::Ok(10)?;
    Ok(val)
}

fn checkErr() -> Result<!, u32> {
    let val = Result::<!, u32>::Err(10)?;
}

fn checkMaybe() -> MyResult<!, !, u8> {
    change_maybe(MyResult::<!, !, u32>::Maybe(10), 0)
}

#[kani::proof]
pub fn harness_residual() {
    let _ = checkMaybe();
    let _ = checkErr();
    let _ = check();
}