Add test for floating point remainder issue

See issue model-checking#2669
reisnera · Aug 12, 2023 · f34a9fb · f34a9fb
1 parent 404fc41
commit f34a9fb
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());
+}