Add test for floating point remainder issue (model-checking#2679)

zhassan-aws · Aug 14, 2023 · f9e2cef · f9e2cef
1 parent 56c724b
commit f9e2cef
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/tests/kani/ArithOperators/rem_float_fixme.rs b/tests/kani/ArithOperators/rem_float_fixme.rs
@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that the remainder operator works with floating point values (see issue #2669)
+
+#[kani::proof]
+fn rem_float() {
+    let dividend = 0.5 * f32::from(kani::any::<i8>());
+    let divisor = 0.5 * f32::from(kani::any::<i8>());
+    kani::assume(divisor != 0.0);
+    let result = dividend % divisor;
+    assert!(result == 0.0 || result.is_normal());
+}