diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 091238811074..a7a3c43edbff 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -113,9 +113,8 @@ impl<'tcx> GotocCtx<'tcx> { _ => Expr::init_unit(self.codegen_ty_stable(*lit_ty), &self.symbol_table), } } - TyConstKind::Bound(..) | TyConstKind::Value(..) => { - unreachable!() - } + TyConstKind::Value(ty, alloc) => self.codegen_allocation(alloc, *ty, span), + TyConstKind::Bound(..) => unreachable!(), TyConstKind::Param(..) | TyConstKind::Unevaluated(..) => { unreachable!() }