diff --git a/tests/kani/Intrinsics/Math/Arith/powi.rs b/tests/kani/Intrinsics/Math/Arith/powi.rs index 70d9d8b0d46b..c7986d18a9ef 100644 --- a/tests/kani/Intrinsics/Math/Arith/powi.rs +++ b/tests/kani/Intrinsics/Math/Arith/powi.rs @@ -5,6 +5,8 @@ fn verify_powi32() { let x: f32 = kani::any(); kani::assume(x.is_normal()); + kani::assume(x >= 1e-19 || x <= -1e-19); + kani::assume(x <= 1.84e19 && x >= -1.84e19); let x2 = x.powi(2); assert!(x2 >= 0.0); } @@ -13,6 +15,8 @@ fn verify_powi32() { fn verify_powi64() { let x: f64 = kani::any(); kani::assume(x.is_normal()); + kani::assume(x >= 1e-153 || x <= -1e-153); + kani::assume(x <= 1.34e154 && x >= -1.34e154); let x2 = x.powi(2); assert!(x2 >= 0.0); }