diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index b6189c070538..8cabd10c87ad 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -611,7 +611,7 @@ impl GotocCtx<'_> {
                 };
                 let layout = self.layout_of(rustc_internal::internal(self.tcx, ty));
                 let expr = match &layout.variants {
-                    Variants::Single { .. } => before.goto_expr,
+                    Variants::Empty | Variants::Single { .. } => before.goto_expr,
                     Variants::Multiple { tag_encoding, .. } => match tag_encoding {
                         TagEncoding::Direct => {
                             let cases = if ty_kind.is_coroutine() {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index d13597794d19..f4ca557afbdb 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -554,6 +554,9 @@ impl GotocCtx<'_> {
             let variant_expr = variant_proj.goto_expr.clone();
             let layout = self.layout_of_stable(res_ty);
             let fields = match &layout.variants {
+                Variants::Empty => {
+                    unreachable!("Aggregate expression for uninhabited enum with no variants")
+                }
                 Variants::Single { index } => {
                     if *index != rustc_internal::internal(self.tcx, variant_index) {
                         // This may occur if all variants except for the one pointed by
@@ -960,6 +963,7 @@ impl GotocCtx<'_> {
     pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty, res_ty: Ty) -> Expr {
         let layout = self.layout_of_stable(ty);
         match &layout.variants {
+            Variants::Empty => unreachable!("Discriminant for uninhabited enum with no variants"),
             Variants::Single { index } => {
                 let discr_val = layout
                     .ty
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 12a61c45b558..90635a71f2e8 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -305,7 +305,7 @@ impl GotocCtx<'_> {
         let variant_index_internal = rustc_internal::internal(self.tcx, variant_index);
         let layout = self.layout_of(dest_ty_internal);
         match &layout.variants {
-            Variants::Single { .. } => Stmt::skip(location),
+            Variants::Empty | Variants::Single { .. } => Stmt::skip(location),
             Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
                 TagEncoding::Direct => {
                     let discr = dest_ty_internal
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 748eb42e7655..88960d40d2ba 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1191,12 +1191,17 @@ impl<'tcx> GotocCtx<'tcx> {
         let layout = self.layout_of(ty);
         // variants appearing in mir code
         match &layout.variants {
+            Variants::Empty => {
+                // an empty enum with no variants (its value cannot be instantiated)
+                self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |_, _| vec![])
+            }
             Variants::Single { index } => {
                 self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, _| {
                     match source_variants.get(*index) {
                         None => {
-                            // an empty enum with no variants (its value cannot be instantiated)
-                            vec![]
+                            unreachable!(
+                                "Enum with no variants must be represented as Variants::Empty"
+                            );
                         }
                         Some(variant) => {
                             // a single enum is pretty much like a struct
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs
index 0a1fc16dcc07..73dce8c2e898 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs
@@ -217,6 +217,7 @@ fn data_bytes_for_ty(
                             // Support basic enumeration forms
                             let ty_variants = def.variants();
                             match layout.variants {
+                                VariantsShape::Empty => Ok(vec![]),
                                 VariantsShape::Single { index } => {
                                     // Only one variant is reachable. This behaves like a struct.
                                     let fields = ty_variants[index.to_index()].fields();
diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
index 2276906aae81..4f5f0530f4cc 100644
--- a/kani-compiler/src/kani_middle/transform/check_values.rs
+++ b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -879,6 +879,7 @@ pub fn ty_validity_per_offset(
                             // Support basic enumeration forms
                             let ty_variants = def.variants();
                             match layout.variants {
+                                VariantsShape::Empty => Ok(vec![]),
                                 VariantsShape::Single { index } => {
                                     // Only one variant is reachable. This behaves like a struct.
                                     let fields = ty_variants[index.to_index()].fields();