Adjust precision

model-checking · Aug 2, 2024 · 9c567a7 · 9c567a7
1 parent 4804c32
commit 9c567a7
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git a/tests/kani/Intrinsics/Math/Arith/log10.rs b/tests/kani/Intrinsics/Math/Arith/log10.rs
@@ -8,7 +8,8 @@ fn verify_log10_32() {
  // log10(10) - 1 == 0
  let abs_difference = (ten.log10() - 1.0).abs();
 
- assert!(abs_difference <= f32::EPSILON);
+ // should be <= f32::EPSILON, but CBMC's approximation of log10 makes results less precise
+ assert!(abs_difference <= 0.03);
 }
 
 #[kani::proof]
@@ -18,5 +19,5 @@ fn verify_log10_64() {
  // log10(100) - 2 == 0
  let abs_difference = (hundred.log10() - 2.0).abs();
 
- assert!(abs_difference < 1e-10);
+ assert!(abs_difference < 0.03);
 }
diff --git a/tests/kani/Intrinsics/Math/Arith/log2.rs b/tests/kani/Intrinsics/Math/Arith/log2.rs
@@ -8,7 +8,8 @@ fn verify_log2_32() {
  // log2(2) - 1 == 0
  let abs_difference = (two.log2() - 1.0).abs();
 
- assert!(abs_difference <= f32::EPSILON);
+ // should be <= f32::EPSILON, but CBMC's approximation of log2 makes results less precise
+ assert!(abs_difference <= 0.09);
 }
 
 #[kani::proof]
@@ -18,5 +19,5 @@ fn verify_log2_64() {
  // log2(4) - 2 == 0
  let abs_difference = (four.log2() - 2.0).abs();
 
- assert!(abs_difference < 1e-10);
+ assert!(abs_difference < 0.09);
 }