// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
#[derive(Debug, PartialEq)]
pub enum Empty {}

#[kani::proof]
fn main() {
    let res: Result<u32, Empty> = Ok(0);
    if let Ok(num) = res {
        num + 1;
    } else {
        3;
    }
}