diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 10822d779b16..a1e807ee4d28 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -848,7 +848,20 @@ impl<'tcx> LayoutOfHelpers<'tcx> for GotocCtx<'tcx, '_> {
 
     #[inline]
     fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: Ty<'tcx>) -> ! {
-        span_bug!(span, "failed to get layout for `{}`: {}", ty, err)
+        // Handle SizeOverflow errors gracefully instead of causing an ICE
+        if let LayoutError::SizeOverflow(_) = err {
+            self.tcx
+                .dcx()
+                .struct_span_err(
+                    span,
+                    format!("values of the type `{}` are too big for the target architecture", ty),
+                )
+                .emit();
+            self.tcx.dcx().abort_if_errors();
+            unreachable!()
+        } else {
+            span_bug!(span, "failed to get layout for `{}`: {}", ty, err)
+        }
     }
 }
 
diff --git a/tests/ui/ice-size-overflow/expected b/tests/ui/ice-size-overflow/expected
new file mode 100644
index 000000000000..65a7e0c80fee
--- /dev/null
+++ b/tests/ui/ice-size-overflow/expected
@@ -0,0 +1,13 @@
+error[E0080]: values of the type `[u8; usize::MAX]` are too big for the target architecture\
+lib/rustlib/src/rust/library/core/src/mem/mod.rs\
+|\
+const SIZE: usize = intrinsics::size_of::<Self>();\
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation of `<S<u8> as std::mem::SizedTypeProperties>::SIZE` failed here\
+
+note: the above error was encountered while instantiating `fn std::mem::size_of::<S<u8>>`\
+tests/ui/ice-size-overflow/large_array.rs\
+|\
+std::mem::size_of::<S<u8>>()\
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to 1 previous error; 1 warning emitted
diff --git a/tests/ui/ice-size-overflow/large_array.rs b/tests/ui/ice-size-overflow/large_array.rs
new file mode 100644
index 000000000000..9127c38042fa
--- /dev/null
+++ b/tests/ui/ice-size-overflow/large_array.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that the compiler handles extremely large array sizes
+//! gracefully with a proper error message instead of causing an ICE.
+//! Previously, this would trigger an internal compiler error at
+//! kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:371:9
+
+struct S<T> {
+    x: [T; !0],
+}
+
+pub fn f() -> usize {
+    std::mem::size_of::<S<u8>>()
+}
+
+#[kani::proof]
+fn main() {
+    let _x = f();
+}