// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
#[kani::proof]
fn main() {
    let a = return_u32();
    assert!(a < 10);
    assert!(return_u32() < 10);
    assert!(return_u64() >= 100);
    assert!(return_bool());
    assert!(return_f32() < 21.0);
    assert!(return_f64() < 11.0 && return_f64() > -11.0);
}
fn return_u32() -> u32 {
    let x: u32 = kani::any();

    if x < 10 {
        return x;
    } else {
        return 5;
    }
}
fn return_u64() -> u64 {
    let x: u64 = kani::any();

    if x > 100 {
        return x;
    } else {
        return 100;
    }
}
fn return_bool() -> bool {
    let x: bool = kani::any();
    if x {
        return x;
    } else {
        return !x;
    }
}
fn return_f32() -> f32 {
    let x = 10.0;
    let y: bool = kani::any();
    if y {
        return x / 2.0;
    } else {
        return x * 2.0;
    }
}
fn return_f64() -> f64 {
    let x: f64 = kani::any();
    if x <= 10.0 && x >= -10.0 {
        return x;
    } else {
        return 0.0;
    }
}