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); }