From 26cdae036ef040412898acc4a6a8c14eb76807ab Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 7 Jun 2024 12:51:10 +0000
Subject: [PATCH] Fix TyConst with TyConstKind Value

---
 kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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!()
             }