From 9c567a792cac59e142fbe254702d8348c184d8ad Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 2 Aug 2024 12:21:42 +0000
Subject: [PATCH] Adjust precision

---
 tests/kani/Intrinsics/Math/Arith/log10.rs | 5 +++--
 tests/kani/Intrinsics/Math/Arith/log2.rs  | 5 +++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/tests/kani/Intrinsics/Math/Arith/log10.rs b/tests/kani/Intrinsics/Math/Arith/log10.rs
index 2d641cde1bcb..4670c72cfeb3 100644
--- 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
index be09bb928d23..52153f8b368a 100644
--- 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);
 }