diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 6f140b67ec84..5d0890e99d2b 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -1017,11 +1017,12 @@ impl Expr {
             IeeeFloatEqual | IeeeFloatNotequal => lhs.typ == rhs.typ && lhs.typ.is_floating_point(),
             // Overflow flags
             OverflowMinus | OverflowResultMinus => {
-                (lhs.typ == rhs.typ && (lhs.typ.is_pointer() || lhs.typ.is_numeric()))
+                (lhs.typ == rhs.typ
+                    && (lhs.typ.is_pointer() || lhs.typ.is_numeric() || lhs.typ.is_vector()))
                     || (lhs.typ.is_pointer() && rhs.typ.is_integer())
             }
             OverflowMult | OverflowPlus | OverflowResultMult | OverflowResultPlus => {
-                (lhs.typ == rhs.typ && lhs.typ.is_integer())
+                (lhs.typ == rhs.typ && (lhs.typ.is_numeric() || lhs.typ.is_vector()))
                     || (lhs.typ.is_pointer() && rhs.typ.is_integer())
             }
             ROk => lhs.typ.is_pointer() && rhs.typ.is_c_size_t(),
diff --git a/tests/kani/SIMD/simd_float_ops_fixme.rs b/tests/kani/SIMD/simd_float_ops.rs
similarity index 64%
rename from tests/kani/SIMD/simd_float_ops_fixme.rs
rename to tests/kani/SIMD/simd_float_ops.rs
index 6b53d95d554a..dbb6d77260b6 100644
--- a/tests/kani/SIMD/simd_float_ops_fixme.rs
+++ b/tests/kani/SIMD/simd_float_ops.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Ensure we can handle SIMD defined in the standard library
-//! FIXME: <https://github.com/model-checking/kani/issues/2631>
 #![allow(non_camel_case_types)]
 #![feature(repr_simd, core_intrinsics, portable_simd)]
 use std::intrinsics::simd::simd_add;
@@ -10,7 +9,7 @@ use std::simd::f32x4;
 
 #[repr(simd)]
 #[derive(Clone, PartialEq, kani::Arbitrary)]
-pub struct f32x2(f32, f32);
+pub struct f32x2([f32; 2]);
 
 impl f32x2 {
     fn as_array(&self) -> &[f32; 2] {
@@ -20,16 +19,22 @@ impl f32x2 {
 
 #[kani::proof]
 fn check_sum() {
-    let a = f32x2(0.0, 0.0);
+    let a = f32x2([0.0, 0.0]);
     let b = kani::any::<f32x2>();
-    let sum = unsafe { simd_add(a.clone(), b) };
-    assert_eq!(sum.as_array(), a.as_array());
+    kani::assume(b.as_array()[0].is_normal());
+    kani::assume(b.as_array()[1].is_normal());
+    let sum = unsafe { simd_add(a.clone(), b.clone()) };
+    assert_eq!(sum.as_array(), b.as_array());
 }
 
 #[kani::proof]
 fn check_sum_portable() {
     let a = f32x4::splat(0.0);
     let b = f32x4::from_array(kani::any());
+    kani::assume(b.as_array()[0].is_normal());
+    kani::assume(b.as_array()[1].is_normal());
+    kani::assume(b.as_array()[2].is_normal());
+    kani::assume(b.as_array()[3].is_normal());
     // Cannot compare them directly: https://github.com/model-checking/kani/issues/2632
     assert_eq!((a + b).as_array(), b.as_array());
 }