From e9ef0f891df7bfcd015428ef1f3dfea6836eba57 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 12:50:15 +0000 Subject: [PATCH] Adjust precision --- tests/kani/Intrinsics/Math/Arith/powi.rs | 4 ++++ 1 file changed, 4 insertions(+) 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); }