diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 417cf04baf5f..51554163fb21 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -394,15 +394,14 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                 }
             }
-            (s, ty::Tuple(substs)) => {
-                // here we have tuples of at most one length
-                if substs.len() == 1 {
-                    let overall_t = self.codegen_ty(ty);
-                    let t = substs[0];
-                    self.codegen_single_variant_single_field(s, span, overall_t, t)
-                } else {
-                    unreachable!()
-                }
+            (Scalar::Int(int), ty::Tuple(_)) => {
+                let int_u128 = int.try_to_uint(int.size()).ok().unwrap();
+                let overall_t = self.codegen_ty(ty);
+                let expr_int = Expr::int_constant(
+                    int_u128,
+                    Type::unsigned_int(overall_t.sizeof_in_bits(&self.symbol_table)),
+                );
+                expr_int.transmute_to(overall_t, &self.symbol_table)
             }
             (_, ty::Array(_, _)) => {
                 // we must have zero size array here
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index d06fabd27b0e..01059ac3ee24 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -13,12 +13,15 @@ use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::MachineModel;
 use cbmc::{btree_string_map, InternString, InternedString};
 use num::bigint::BigInt;
+use rustc_index::vec::IndexVec;
 use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
 use rustc_middle::ty::adjustment::PointerCast;
 use rustc_middle::ty::layout::LayoutOf;
-use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
-use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants};
+use rustc_middle::ty::{self, AdtDef, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
+use rustc_target::abi::{FieldsShape, LayoutS, Size, TagEncoding, VariantIdx, Variants};
+use std::cmp::Ordering;
 use std::collections::BTreeMap;
+use std::iter::Peekable;
 use tracing::{debug, warn};
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -279,6 +282,385 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    fn codegen_rvalue_enum_single(
+        &mut self,
+        variant_index: &VariantIdx,
+        operands: &[Operand<'tcx>],
+        overall_t: Type,
+        adt: &AdtDef<'_>,
+    ) -> Expr {
+        // TODO: IMHO the type codegen should be modified as there are multiple types here,
+        // it's just that there is only a single _binary_ layout
+        let variant = &adt.variants()[*variant_index];
+        let components = overall_t.lookup_components(&self.symbol_table).unwrap().clone();
+        Expr::struct_expr_with_nondet_fields(
+            overall_t,
+            variant
+                .fields
+                .iter()
+                .zip(operands.iter().zip(components.iter()))
+                .filter_map(|(f, (o, c))| {
+                    let op_expr = self.codegen_operand(o);
+                    let op_width = op_expr.typ().sizeof_in_bits(&self.symbol_table);
+                    if op_width == 0 {
+                        None
+                    } else {
+                        Some((
+                            InternedString::from(f.name.to_string()),
+                            op_expr.transmute_to(c.typ(), &self.symbol_table),
+                        ))
+                    }
+                })
+                .collect(),
+            &self.symbol_table,
+        )
+    }
+
+    fn codegen_rvalue_enum_direct(
+        &mut self,
+        variant_index: &VariantIdx,
+        operands: &[Operand<'tcx>],
+        overall_t: Type,
+        adt: &AdtDef<'_>,
+        variants: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
+    ) -> Expr {
+        let fields = overall_t.lookup_components(&self.symbol_table).unwrap().clone();
+        assert_eq!(fields.len(), 2, "TagEncoding::Direct encountered for enum with empty variants");
+        assert_eq!(
+            fields[0].name().to_string(),
+            "case",
+            "Unexpected field in enum/generator. Please report your failing case at https://github.com/model-checking/kani/issues/1465"
+        );
+        let case_value = Expr::int_constant(variant_index.index(), fields[0].typ());
+        assert_eq!(
+            fields[1].name().to_string(),
+            "cases",
+            "Unexpected field in enum/generator. Please report your failing case at https://github.com/model-checking/kani/issues/1465"
+        );
+        assert!(matches!(variants[*variant_index].variants, Variants::Single { .. }));
+        let variant = &adt.variants()[*variant_index];
+        if variant.fields.is_empty() {
+            Expr::struct_expr_with_nondet_fields(
+                overall_t,
+                btree_string_map![("case", case_value)],
+                &self.symbol_table,
+            )
+        } else {
+            let target_component = fields[1]
+                .typ()
+                .lookup_field(variant.name.to_string(), &self.symbol_table)
+                .unwrap()
+                .clone();
+            let cases_value = Expr::union_expr(
+                fields[1].typ(),
+                target_component.name(),
+                Expr::struct_expr_from_values(
+                    target_component.typ(),
+                    variants[*variant_index]
+                        .fields
+                        .index_by_increasing_offset()
+                        .map(|idx| self.codegen_operand(&operands[idx]))
+                        .collect(),
+                    &self.symbol_table,
+                ),
+                &self.symbol_table,
+            );
+            Expr::struct_expr_from_values(
+                overall_t,
+                vec![case_value, cases_value],
+                &self.symbol_table,
+            )
+        }
+    }
+
+    fn codegen_niche_struct_from_operands_rec(
+        &mut self,
+        operands_iter: &mut Peekable<std::slice::Iter<'_, Expr>>,
+        operands_base_offset: u64,
+        niche_value_u128: u128,
+        niche_offset_bits: u64,
+        untagged_type: &Type,
+        target_offset_bits: &mut u64,
+    ) -> Expr {
+        let untagged_fields = untagged_type.lookup_components(&self.symbol_table).unwrap().clone();
+        let mut exprs: BTreeMap<InternedString, Expr> = BTreeMap::new();
+        for comp in untagged_fields {
+            let comp_size_bits = comp.typ().sizeof_in_bits(&self.symbol_table);
+            if comp_size_bits == 0 {
+                continue;
+            }
+
+            if *target_offset_bits == niche_offset_bits {
+                exprs.insert(
+                    comp.name(),
+                    if comp.typ().is_integer() {
+                        Expr::int_constant(niche_value_u128, comp.typ())
+                    } else {
+                        let niche_value_expr = Expr::int_constant(
+                            niche_value_u128,
+                            Type::unsigned_int(comp.typ().sizeof_in_bits(&self.symbol_table)),
+                        );
+                        niche_value_expr.transmute_to(comp.typ(), &self.symbol_table)
+                    },
+                );
+            } else if *target_offset_bits >= operands_base_offset && operands_iter.peek().is_some()
+            {
+                let operand = operands_iter.peek().unwrap();
+                let operand_size_bits = operand.typ().sizeof_in_bits(&self.symbol_table);
+                debug!(?operand_size_bits, "OPERAND BITS");
+                match operand_size_bits.cmp(&comp_size_bits) {
+                    Ordering::Less => {
+                        if comp.typ().is_struct_tag() {
+                            // recurse
+                            exprs.insert(
+                                comp.name(),
+                                self.codegen_niche_struct_from_operands_rec(
+                                    operands_iter,
+                                    operands_base_offset,
+                                    niche_value_u128,
+                                    niche_offset_bits,
+                                    &comp.typ(),
+                                    target_offset_bits,
+                                ),
+                            );
+                        } else if comp.typ().is_union_tag() {
+                            // TODO: this is reached in the std-lib regression test -- find the
+                            // maximum member and use that member as target component instead, then
+                            // wrap in union expr
+                            unimplemented!()
+                        } else if comp.typ().is_array() {
+                            // TODO: this is reached in the firecracker regression test -- update
+                            // each array element, might try to use a single element for a start
+                            unimplemented!()
+                        } else {
+                            // TODO: we really need to concatenate the operand with nondet bits
+                            exprs.insert(
+                                comp.name(),
+                                operands_iter
+                                    .next()
+                                    .unwrap()
+                                    .clone()
+                                    .transmute_to(
+                                        Type::unsigned_int(operand_size_bits),
+                                        &self.symbol_table,
+                                    )
+                                    .cast_to(comp.typ()),
+                            );
+                        }
+                    }
+                    Ordering::Equal => {
+                        exprs.insert(
+                            comp.name(),
+                            operands_iter
+                                .next()
+                                .unwrap()
+                                .clone()
+                                .transmute_to(comp.typ(), &self.symbol_table),
+                        );
+                    }
+                    Ordering::Greater => {
+                        // TODO: we also need to store the remaining bits by taking an offset _into
+                        // the same operand_ -- tests/kani/Slice/pathbuf.rs still passes for now,
+                        // but we are actually losing information here
+                        exprs.insert(
+                            comp.name(),
+                            operands_iter.next().unwrap().clone().reinterpret_cast(comp.typ()),
+                        );
+                    }
+                }
+            } else if niche_offset_bits < *target_offset_bits + comp_size_bits {
+                if comp.typ().is_struct_tag() {
+                    // recurse
+                    exprs.insert(
+                        comp.name(),
+                        self.codegen_niche_struct_from_operands_rec(
+                            operands_iter,
+                            operands_base_offset,
+                            niche_value_u128,
+                            niche_offset_bits,
+                            &comp.typ(),
+                            target_offset_bits,
+                        ),
+                    );
+                } else {
+                    exprs.insert(
+                        comp.name(),
+                        Expr::int_constant(
+                            niche_value_u128,
+                            Type::unsigned_int(comp.typ().sizeof_in_bits(&self.symbol_table)),
+                        )
+                        .transmute_to(comp.typ(), &self.symbol_table),
+                    );
+                }
+            }
+            *target_offset_bits += comp_size_bits;
+        }
+        Expr::struct_expr_with_nondet_fields(untagged_type.clone(), exprs, &self.symbol_table)
+    }
+
+    fn codegen_rvalue_enum(
+        &mut self,
+        variant_index: &VariantIdx,
+        operands: &[Operand<'tcx>],
+        ty: Ty<'tcx>,
+    ) -> Expr {
+        let overall_t = self.codegen_ty(ty);
+        let layout = self.layout_of(ty);
+        let adt = match &ty.kind() {
+            ty::Adt(adt, _) => adt,
+            _ => unreachable!(),
+        };
+        match &layout.variants {
+            Variants::Single { .. } => {
+                self.codegen_rvalue_enum_single(variant_index, operands, overall_t, adt)
+            }
+            Variants::Multiple { tag_encoding: TagEncoding::Direct, variants, .. } => {
+                self.codegen_rvalue_enum_direct(variant_index, operands, overall_t, adt, variants)
+            }
+            Variants::Multiple {
+                tag_encoding:
+                    TagEncoding::Niche { untagged_variant, ref niche_variants, niche_start },
+                variants,
+                tag_field,
+                ..
+            } => {
+                // 1. Find the type of the member corresponding to the variant index.
+                // 2. Create a (possibly empty) struct of the type corresponding to the variant
+                //    using the available operands.
+                // 3. If this is the untagged variant, then we are done: just create a struct or
+                //    union (cf. codegen_enum_niche) and return the result.
+                // 4. Else, transmute to the members of the untagged variant starting from the
+                //    desired offset; also set the niche by niche member name; leave the remainder
+                //    nondet. In doing so, we may need to recurse into the component types of the
+                //    untagged variant.
+                let variant = &adt.variants()[*variant_index];
+                let variant_layout = &variants[*variant_index];
+                // from codegen_enum_niche
+                let non_zst_count =
+                    variants.iter().filter(|layout| layout.size.bytes() > 0).count();
+                if variant_index == untagged_variant {
+                    let target_component = overall_t
+                        .lookup_field(variant.name.to_string(), &self.symbol_table)
+                        .unwrap()
+                        .clone();
+                    let member_expr = Expr::struct_expr_from_values(
+                        target_component.typ(),
+                        variant_layout
+                            .fields
+                            .index_by_increasing_offset()
+                            .map(|idx| self.codegen_operand(&operands[idx]))
+                            .collect(),
+                        &self.symbol_table,
+                    );
+                    if non_zst_count > 1 {
+                        Expr::union_expr(
+                            overall_t,
+                            target_component.name(),
+                            member_expr,
+                            &self.symbol_table,
+                        )
+                    } else {
+                        Expr::struct_expr_with_nondet_fields(
+                            overall_t,
+                            btree_string_map![(target_component.name(), member_expr)],
+                            &self.symbol_table,
+                        )
+                    }
+                } else {
+                    let untagged_variant_info = &adt.variants()[*untagged_variant];
+                    let untagged_target_component = overall_t
+                        .lookup_field(untagged_variant_info.name.to_string(), &self.symbol_table)
+                        .unwrap()
+                        .clone();
+                    let niche_offset_bits = layout.fields.offset(*tag_field).bits();
+                    // compute the niche value like the SSA back-end does in codegen_set_discr
+                    let niche_value = variant_index.index() - niche_variants.start().index();
+                    let niche_value_u128 = (niche_value as u128).wrapping_add(*niche_start);
+                    let variant_operands: Vec<_> = variant_layout
+                        .fields
+                        .index_by_increasing_offset()
+                        .filter_map(|idx| {
+                            let o = &operands[idx];
+                            let oty = self.operand_ty(o);
+                            let o_layout = self.layout_of(oty);
+                            if o_layout.size.bytes() == 0 {
+                                None
+                            } else {
+                                Some(self.codegen_operand(o))
+                            }
+                        })
+                        .collect();
+                    let mut operands_base_offset: u64 = 0;
+                    if let FieldsShape::Arbitrary { offsets, .. } = &variant_layout.fields {
+                        let mut indices = variant_layout.fields.index_by_increasing_offset();
+                        if let Some(idx) = indices.next() {
+                            operands_base_offset = offsets[idx].bits();
+                        }
+                    } else {
+                        unreachable!();
+                    }
+                    let mut starting_offset: u64 = 0;
+                    let untagged_member_expr = self.codegen_niche_struct_from_operands_rec(
+                        &mut variant_operands.iter().peekable(),
+                        operands_base_offset,
+                        niche_value_u128,
+                        niche_offset_bits,
+                        &untagged_target_component.typ(),
+                        &mut starting_offset,
+                    );
+                    if non_zst_count > 1 {
+                        Expr::union_expr(
+                            overall_t,
+                            untagged_target_component.name(),
+                            untagged_member_expr,
+                            &self.symbol_table,
+                        )
+                    } else {
+                        Expr::struct_expr_with_nondet_fields(
+                            overall_t,
+                            btree_string_map![(
+                                untagged_target_component.name(),
+                                untagged_member_expr
+                            )],
+                            &self.symbol_table,
+                        )
+                    }
+                }
+            }
+        }
+    }
+
+    fn codegen_rvalue_generator(&mut self, operands: &[Operand<'tcx>], ty: Ty<'tcx>) -> Expr {
+        let overall_t = self.codegen_ty(ty);
+        let direct_fields = overall_t.lookup_field("direct_fields", &self.symbol_table).unwrap();
+        let direct_fields_components =
+            direct_fields.typ().lookup_components(&self.symbol_table).unwrap().clone();
+        let mut operands_iter = operands.iter();
+        let direct_fields_expr = Expr::struct_expr_with_nondet_fields(
+            direct_fields.typ(),
+            direct_fields_components
+                .iter()
+                .filter_map(|c| {
+                    if c.is_padding() {
+                        None
+                    } else {
+                        Some((
+                            c.name(),
+                            if c.name() == "case" {
+                                Expr::int_constant(0, c.typ())
+                            } else {
+                                self.codegen_operand(operands_iter.next().unwrap())
+                            },
+                        ))
+                    }
+                })
+                .collect(),
+            &self.symbol_table,
+        );
+        assert!(operands_iter.next().is_none());
+        Expr::union_expr(overall_t, "direct_fields", direct_fields_expr, &self.symbol_table)
+    }
+
     fn codegen_rvalue_aggregate(
         &mut self,
         k: &AggregateKind<'tcx>,
@@ -304,20 +686,72 @@ impl<'tcx> GotocCtx<'tcx> {
                     )
                 }
             }
-            AggregateKind::Tuple => Expr::struct_expr_from_values(
-                self.codegen_ty(res_ty),
-                operands
-                    .iter()
-                    .filter_map(|o| {
-                        let oty = self.operand_ty(o);
-                        if oty.is_unit() { None } else { Some(self.codegen_operand(o)) }
-                    })
-                    .collect(),
-                &self.symbol_table,
-            ),
-            AggregateKind::Adt(_, _, _, _, _) => unimplemented!(),
-            AggregateKind::Closure(_, _) => unimplemented!(),
-            AggregateKind::Generator(_, _, _) => unimplemented!(),
+            AggregateKind::Tuple => {
+                let layout = self.layout_of(res_ty);
+                Expr::struct_expr_from_values(
+                    self.codegen_ty(res_ty),
+                    layout
+                        .fields
+                        .index_by_increasing_offset()
+                        .map(|idx| self.codegen_operand(&operands[idx]))
+                        .collect(),
+                    &self.symbol_table,
+                )
+            }
+            AggregateKind::Adt(_, _, _, _, Some(active_field_index)) => {
+                assert!(res_ty.is_union());
+                assert_eq!(operands.len(), 1);
+                let typ = self.codegen_ty(res_ty);
+                let components = typ.lookup_components(&self.symbol_table).unwrap();
+                Expr::union_expr(
+                    typ,
+                    components[active_field_index].name(),
+                    self.codegen_operand(&operands[0]),
+                    &self.symbol_table,
+                )
+            }
+            AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => {
+                let typ = self.codegen_ty(res_ty);
+                let layout = self.layout_of(res_ty);
+                Expr::vector_expr(
+                    typ,
+                    layout
+                        .fields
+                        .index_by_increasing_offset()
+                        .map(|idx| self.codegen_operand(&operands[idx]))
+                        .collect(),
+                )
+            }
+            AggregateKind::Adt(_, variant_index, _, _, _) if res_ty.is_enum() => {
+                self.codegen_rvalue_enum(&variant_index, &operands, res_ty)
+            }
+            AggregateKind::Adt(_, _, _, _, _) => {
+                let typ = self.codegen_ty(res_ty);
+                let layout = self.layout_of(res_ty);
+                Expr::struct_expr_from_values(
+                    typ,
+                    layout
+                        .fields
+                        .index_by_increasing_offset()
+                        .map(|idx| self.codegen_operand(&operands[idx]))
+                        .collect(),
+                    &self.symbol_table,
+                )
+            }
+            AggregateKind::Closure(_, _) => {
+                let typ = self.codegen_ty(res_ty);
+                let layout = self.layout_of(res_ty);
+                Expr::struct_expr_from_values(
+                    typ,
+                    layout
+                        .fields
+                        .index_by_increasing_offset()
+                        .map(|idx| self.codegen_operand(&operands[idx]))
+                        .collect(),
+                    &self.symbol_table,
+                )
+            }
+            AggregateKind::Generator(_, _, _) => self.codegen_rvalue_generator(&operands, res_ty),
         }
     }
 
diff --git a/tests/kani/Enum/one_two.rs b/tests/kani/Enum/one_two.rs
new file mode 100644
index 000000000000..54b2dc8bbc0b
--- /dev/null
+++ b/tests/kani/Enum/one_two.rs
@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+enum Niche_Enum {
+    One(bool),
+    Two(bool, bool),
+}
+
+enum Enum {
+    One(u32),
+    Two(u32, u32),
+}
+
+#[kani::proof]
+fn check() {
+    // This will have one operand.
+    let _var = Niche_Enum::One(false);
+    // This will have two operands -- true and false
+    let _var = Niche_Enum::Two(true, false);
+    // This will have one operand.
+    let _var = Enum::One(1);
+    // This will have two operands -- 2 and 3
+    let _var = Enum::Two(2, 3);
+}