More precise bounds

tautschnig · Feb 7, 2024 · bc5ef1f · bc5ef1f
1 parent 22d33e3
commit bc5ef1f
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/tests/kani/Intrinsics/Math/Arith/exp.rs b/tests/kani/Intrinsics/Math/Arith/exp.rs
@@ -11,7 +11,7 @@ fn verify_exp32() {
     let two_sq = std::f32::consts::E * std::f32::consts::E;
     let two_exp = two.exp();
 
-    assert!((two_sq - two_exp).abs() <= 1.0);
+    assert!((two_sq - two_exp).abs() <= 0.192);
 }
 
 #[kani::proof]
@@ -20,5 +20,5 @@ fn verify_exp64() {
     let two_sq = std::f64::consts::E * std::f64::consts::E;
     let two_exp = two.exp();
 
-    assert!((two_sq - two_exp).abs() <= 1.0);
+    assert!((two_sq - two_exp).abs() <= 0.192);
 }
diff --git a/tests/kani/Intrinsics/Math/Arith/exp2.rs b/tests/kani/Intrinsics/Math/Arith/exp2.rs
@@ -10,13 +10,13 @@ fn verify_exp2_32() {
     let two = 2.0_f32;
     let two_two = two.exp2();
 
-    assert!((two_two - 4.0).abs() <= 1.0);
+    assert!((two_two - 4.0).abs() <= 0.345);
 }
 
 #[kani::proof]
 fn verify_exp2_64() {
     let two = 2.0_f64;
     let two_two = two.exp2();
 
-    assert!((two_two - 4.0).abs() <= 1.0);
+    assert!((two_two - 4.0).abs() <= 0.345);
 }
diff --git a/tests/kani/Intrinsics/Math/Arith/log.rs b/tests/kani/Intrinsics/Math/Arith/log.rs
@@ -10,13 +10,13 @@ fn verify_logf32() {
     let e = std::f32::consts::E;
     let e_log = e.ln();
 
-    assert!((e_log - 1.0).abs() <= 0.1);
+    assert!((e_log - 1.0).abs() <= 0.058);
 }
 
 #[kani::proof]
 fn verify_logf64() {
     let e = std::f64::consts::E;
     let e_log = e.ln();
 
-    assert!((e_log - 1.0).abs() <= 0.1);
+    assert!((e_log - 1.0).abs() <= 0.058);
 }