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

// Test that checks for UNREACHABLE panics. The panic is reported as NONE for the assumption that the divisor is not zero.
fn divide(a: i32, b: i32) -> i32 {
    if b != 0 {
        return a / b;
    } else {
        panic!("Division by zero");
    }
}

#[kani::proof]
fn main() {
    let y: i32 = kani::any();
    kani::assume(y != 0);
    let result = divide(10, y);
    assert_eq!(result, 5);
}