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

// kani-flags: --enable-unstable --concrete-playback=print

/// Note: Don't include NaN because there are multiple possible NaN values.
#[kani::proof]
pub fn harness() {
    let f32_1: f32 = kani::any();
    let f32_2: f32 = kani::any();
    let f32_3: f32 = kani::any();
    let f32_4: f32 = kani::any();
    let f32_5: f32 = kani::any();
    let f32_6: f32 = kani::any();
    let f32_7: f32 = kani::any();
    let f32_8: f32 = kani::any();
    assert!(
        !(f32_1 == f32::NEG_INFINITY
            && f32_2 == f32::MIN
            && f32_3 == -101f32
            && (f32_4 == 0f32 && f32_4.signum() < 0.0)
            && f32_5 == f32::MIN_POSITIVE
            && f32_6 == 101f32
            && f32_7 == f32::MAX
            && f32_8 == f32::INFINITY)
    );
}