diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 4e10cb98c650..b6050d915666 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -233,7 +233,6 @@ impl KaniSession {
             args.push("--no-pointer-check".into());
         }
         if self.args.checks.overflow_on() {
-            args.push("--float-overflow-check".into());
             args.push("--nan-check".into());
 
             // TODO: Implement conversion checks as an optional check.
diff --git a/tests/ui/cbmc_checks/float-overflow/expected b/tests/ui/cbmc_checks/float-overflow/check_message.expected
similarity index 100%
rename from tests/ui/cbmc_checks/float-overflow/expected
rename to tests/ui/cbmc_checks/float-overflow/check_message.expected
diff --git a/tests/ui/cbmc_checks/float-overflow/check_message.rs b/tests/ui/cbmc_checks/float-overflow/check_message.rs
index 590a2be20230..229bc373a883 100644
--- a/tests/ui/cbmc_checks/float-overflow/check_message.rs
+++ b/tests/ui/cbmc_checks/float-overflow/check_message.rs
@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
+// kani-flags: --enable-unstable --cbmc-args --float-overflow-check
 // Check we don't print temporary variables as part of CBMC messages.
 extern crate kani;
 
diff --git a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected
new file mode 100644
index 000000000000..880f00714b32
--- /dev/null
+++ b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
\ No newline at end of file
diff --git a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs
new file mode 100644
index 000000000000..5b57e4b4377d
--- /dev/null
+++ b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// This test verifies that Kani does not report floating-point overflow by default
+// for operations that result in +/-Infinity.
+extern crate kani;
+
+// Use the result so rustc doesn't optimize them away.
+fn dummy(result: f32) -> f32 {
+    result
+}
+
+#[kani::proof]
+fn main() {
+    let a = kani::any_where(|&x: &f32| x.is_finite());
+    let b = kani::any_where(|&x: &f32| x.is_finite());
+
+    dummy(a + b);
+    dummy(a - b);
+    dummy(a * b);
+    dummy(-a);
+}