From 37085346dcec64b50ffec7262c826cd42ebed059 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 14:10:47 +0000 Subject: [PATCH] Don't run into early NaN --- tests/kani/Intrinsics/Math/Arith/sqrt.rs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/tests/kani/Intrinsics/Math/Arith/sqrt.rs b/tests/kani/Intrinsics/Math/Arith/sqrt.rs index d9003ae8d066..31afaba8a740 100644 --- a/tests/kani/Intrinsics/Math/Arith/sqrt.rs +++ b/tests/kani/Intrinsics/Math/Arith/sqrt.rs @@ -4,25 +4,21 @@ #[kani::proof] fn verify_sqrt32() { let positive = 4.0_f32; - let negative = -4.0_f32; let negative_zero = -0.0_f32; let abs_difference = (positive.sqrt() - 2.0).abs(); assert!(abs_difference <= f32::EPSILON); - assert!(negative.sqrt().is_nan()); assert!(negative_zero.sqrt() == negative_zero); } #[kani::proof] fn verify_sqrt64() { let positive = 4.0_f64; - let negative = -4.0_f64; let negative_zero = -0.0_f64; let abs_difference = (positive.sqrt() - 2.0).abs(); assert!(abs_difference <= 1e-10); - assert!(negative.sqrt().is_nan()); assert!(negative_zero.sqrt() == negative_zero); }