Adjust precision

model-checking · Aug 2, 2024 · e9ef0f8 · e9ef0f8
1 parent 767d454
commit e9ef0f8
Showing 1 changed file with 4 additions and 0 deletions.
diff --git 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);
 }