remove flag float-overflow-check

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.

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;
 

tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check we don't print temporary variables as part of CBMC messages.
+extern crate kani;
+
+use kani::any;
+
+// 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() && x.abs() < 1e20);
+    let b = kani::any_where(|&x: &f32| x.is_finite() && x.abs() < 1e20);
+
+    dummy(a + b);
+    dummy(a - b);
+    dummy(a * b);
+    dummy(-a);
+}