From f9e2cefe4a07c44f015fd984c0861cd0e74d3e8d Mon Sep 17 00:00:00 2001
From: Alex Reisner <1683937+reisnera@users.noreply.github.com>
Date: Mon, 14 Aug 2023 17:22:04 -0500
Subject: [PATCH] Add test for floating point remainder issue (#2679)

---
 tests/kani/ArithOperators/rem_float_fixme.rs | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 tests/kani/ArithOperators/rem_float_fixme.rs

diff --git a/tests/kani/ArithOperators/rem_float_fixme.rs b/tests/kani/ArithOperators/rem_float_fixme.rs
new file mode 100644
index 000000000000..42bd1fc8e532
--- /dev/null
+++ 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());
+}