Skip to content

Commit

Permalink
Don't run into early NaN
Browse files Browse the repository at this point in the history
  • Loading branch information
tautschnig committed Aug 2, 2024
1 parent 96ad019 commit 3708534
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions tests/kani/Intrinsics/Math/Arith/sqrt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}

0 comments on commit 3708534

Please sign in to comment.