diff --git a/boogie_ast/src/boogie_program/mod.rs b/boogie_ast/src/boogie_program/mod.rs
index fc9fc85c6d10..d62735eeefc4 100644
--- a/boogie_ast/src/boogie_program/mod.rs
+++ b/boogie_ast/src/boogie_program/mod.rs
@@ -138,6 +138,9 @@ pub enum BinaryOp {
 
     /// Modulo
     Mod,
+
+    /// Bit-Vector Concat
+    Concat,
 }
 
 /// Expr types
@@ -155,6 +158,9 @@ pub enum Expr {
     /// Binary operation
     BinaryOp { op: BinaryOp, left: Box<Expr>, right: Box<Expr> },
 
+    /// Bit-vector extract operation, e.g. `x[7:2]` (half-open interval)
+    Extract { base: Box<Expr>, high: usize, low: usize },
+
     /// Function call
     FunctionCall { symbol: String, arguments: Vec<Expr> },
 
@@ -170,9 +176,26 @@ impl Expr {
         Expr::Literal(l)
     }
 
+    pub fn concat(e1: Box<Expr>, e2: Box<Expr>) -> Self {
+        Expr::BinaryOp { op: BinaryOp::Concat, left: e1, right: e2 }
+    }
+
+    pub fn extract(base: Box<Expr>, high: usize, low: usize) -> Self {
+        Expr::Extract { base, high, low }
+    }
+
     pub fn function_call(symbol: String, arguments: Vec<Expr>) -> Self {
         Expr::FunctionCall { symbol, arguments }
     }
+
+    pub fn sign_extend(e: Box<Expr>, _width: usize) -> Self {
+        let _e = e;
+        todo!()
+    }
+
+    pub fn zero_extend(e: Box<Expr>, width: usize) -> Self {
+        Expr::concat(Box::new(Expr::literal(Literal::bv(width, 0.into()))), e)
+    }
 }
 
 impl ToString for Expr {
diff --git a/boogie_ast/src/boogie_program/writer.rs b/boogie_ast/src/boogie_program/writer.rs
index 5464aa0eabc1..85c2f84fcd2d 100644
--- a/boogie_ast/src/boogie_program/writer.rs
+++ b/boogie_ast/src/boogie_program/writer.rs
@@ -300,6 +300,11 @@ impl Expr {
                 right.write_to(writer)?;
                 write!(writer, ")")?;
             }
+            Expr::Extract { base, high, low } => {
+                write!(writer, "(")?;
+                base.write_to(writer)?;
+                write!(writer, ")[{high}:{low}]")?;
+            }
             Expr::FunctionCall { symbol, arguments } => {
                 write!(writer, "{symbol}(")?;
                 for (i, a) in arguments.iter().enumerate() {
@@ -521,6 +526,7 @@ impl BinaryOp {
             BinaryOp::Gt => write!(writer, ">")?,
             BinaryOp::Lte => write!(writer, "<=")?,
             BinaryOp::Gte => write!(writer, ">=")?,
+            BinaryOp::Concat => write!(writer, "++")?,
         }
         Ok(())
     }
diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
index 103d5e14c59d..bdd66f9b7ffe 100644
--- a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
+++ b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use itertools::Itertools;
+use std::cmp::Ordering;
 use std::io::Write;
 
 use crate::kani_queries::QueryDb;
@@ -13,7 +14,7 @@ use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::mir::interpret::Scalar;
 use rustc_middle::mir::traversal::reverse_postorder;
 use rustc_middle::mir::{
-    BasicBlock, BasicBlockData, BinOp, Body, Const as mirConst, ConstOperand, ConstValue,
+    BasicBlock, BasicBlockData, BinOp, Body, CastKind, Const as mirConst, ConstOperand, ConstValue,
     HasLocalDecls, Local, Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind,
     SwitchTargets, Terminator, TerminatorKind, UnOp, VarDebugInfoContents,
 };
@@ -321,6 +322,28 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
                 // TODO: handle overflow check
                 self.codegen_binary_op(binop, e1, e2)
             }
+            Rvalue::Cast(kind, operand, ty) => {
+                if *kind == CastKind::IntToInt {
+                    let from_type = self.operand_ty(operand);
+                    let o = self.codegen_operand(operand);
+                    let from = self.codegen_type(from_type);
+                    let to = self.codegen_type(*ty);
+                    let Type::Bv(from_width) = from else { panic!("Expecting bv type in cast") };
+                    let Type::Bv(to_width) = to else { panic!("Expecting bv type in cast") };
+                    let op = match from_width.cmp(&to_width) {
+                        Ordering::Greater => Expr::extract(Box::new(o), to_width, 0),
+                        Ordering::Less => match from_type.kind() {
+                            ty::Int(_) => Expr::sign_extend(Box::new(o), to_width - from_width),
+                            ty::Uint(_) => Expr::zero_extend(Box::new(o), to_width - from_width),
+                            _ => todo!(),
+                        },
+                        Ordering::Equal => o,
+                    };
+                    (None, op)
+                } else {
+                    todo!()
+                }
+            }
             _ => todo!(),
         }
     }
diff --git a/tests/script-based-boogie/unbounded_array_serde/config.yml b/tests/script-based-boogie/unbounded_array_serde/config.yml
new file mode 100644
index 000000000000..2e9f6c922a1e
--- /dev/null
+++ b/tests/script-based-boogie/unbounded_array_serde/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: gen_boogie_and_dump.sh
+expected: expected
diff --git a/tests/script-based-boogie/unbounded_array_serde/expected b/tests/script-based-boogie/unbounded_array_serde/expected
new file mode 100644
index 000000000000..65e43351db32
--- /dev/null
+++ b/tests/script-based-boogie/unbounded_array_serde/expected
@@ -0,0 +1,69 @@
+// Datatypes:
+datatype $Array<T> { $Array(data: [bv64]T, len: bv64) }
+
+// Functions:
+function {:bvbuiltin "bvult"} $BvUnsignedLessThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvslt"} $BvSignedLessThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvugt"} $BvUnsignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvsgt"} $BvSignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvadd"} $BvAdd<T>(lhs: T, rhs: T) returns (T);
+
+function {:bvbuiltin "bvor"} $BvOr<T>(lhs: T, rhs: T) returns (T);
+
+function {:bvbuiltin "bvand"} $BvAnd<T>(lhs: T, rhs: T) returns (T);
+
+function {:bvbuiltin "bvshl"} $BvShl<T>(lhs: T, rhs: T) returns (T);
+
+function {:bvbuiltin "bvlshr"} $BvShr<T>(lhs: T, rhs: T) returns (T);
+
+// Procedures:
+procedure
+{
+  var src: $Array bv16;
+  var buf: $Array bv8;
+  var src_len: bv64;
+  var buf_len: bv64;
+  var i: bv64;
+  var x: bv16;
+  var byte0: bv8;
+  var byte1: bv8;
+  var j: bv64;
+  var dst: $Array bv16;
+  bb
+  havoc src; 
+  goto bb
+  havoc buf; 
+  src_len := src->len;
+  buf_len := buf->len;
+  := $BvShr(buf_len, 1bv64);
+  := !($BvUnsignedLessThan(
+  assume
+  i := 0bv64;
+  := $BvUnsignedLessThan(
+  if (\
+    goto bb\
+  } else {
+    goto bb\
+  }
+  havoc dst; 
+  return;
+  := src->data[
+  := dst->data[
+  assert
+  := $BvAdd(i, 1bv64);
+  := $BvShl(
+  := buf->data[
+  := (0bv8 ++
+  := $BvOr(
+  := $BvAnd(x, 255bv16);
+  )[8:0];
+  := $BvShr(x, 8bv16);
+  byte1 :=
+  j := $BvShl(
+  buf->data[(j)] := byte0;
+  := $BvAdd(j, 1bv64);
+}
diff --git a/tests/script-based-boogie/unbounded_array_serde/gen_boogie_and_dump.sh b/tests/script-based-boogie/unbounded_array_serde/gen_boogie_and_dump.sh
new file mode 100755
index 000000000000..0233ad780871
--- /dev/null
+++ b/tests/script-based-boogie/unbounded_array_serde/gen_boogie_and_dump.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+# Delete any leftover Boogie files
+rm *.bpl
+
+echo "[TEST] Run verification..."
+kani -Zboogie test.rs
+
+cat *.bpl
diff --git a/tests/script-based-boogie/unbounded_array_serde/test.rs b/tests/script-based-boogie/unbounded_array_serde/test.rs
new file mode 100644
index 000000000000..017c36050878
--- /dev/null
+++ b/tests/script-based-boogie/unbounded_array_serde/test.rs
@@ -0,0 +1,50 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! A test that demonstrates unbounded verification of array-based programs.
+//! The test uses `any_array` which creates arrays with non-deterministic
+//! content and length.
+//! The `src` array of words is serialized into the `buf` byte array and then
+//! deserialized back into `dst`.
+//! The test checks that the round trip of serialization and deserialization is
+//! the identity.
+
+#[kani::proof]
+fn serde() {
+    let src = kani::array::any_array::<u16>();
+    let mut buf = kani::array::any_array::<u8>();
+    let src_len: usize = src.len();
+    let buf_len: usize = buf.len();
+    kani::assume(buf_len >> 1u64 >= src_len);
+
+    // serialize
+    let mut i: usize = 0;
+    //Loop_invariant: forall j: usize :: j < i => ((buf[j << 1u64 + 1] ++ buf[j << 1u64]) == src[j])
+    while i < src_len {
+        let x = src[i];
+        let byte0: u8 = (x & 0xFF) as u8;
+        let byte1: u8 = ((x >> 8u16) & 0xFF) as u8;
+        let j: usize = i << 1u64;
+        buf[j] = byte0;
+        buf[j + 1] = byte1;
+        i += 1;
+    }
+
+    // deserialize
+    let mut dst = kani::array::any_array::<u16>();
+    kani::assume(dst.len() >= src_len);
+    i = 0;
+    //Loop_invariant: forall j: usize :: j < i => ((buf[j << 1u64 + 1] ++ buf[j << 1u64]) == dst[j])
+    while i < src_len {
+        let j: usize = i << 1u64;
+        dst[i] = ((buf[j + 1] as u16) << 8u16) | (buf[j] as u16);
+        i += 1;
+    }
+
+    // Check the round trip
+    i = 0;
+    while i < src_len {
+        kani::assert(src[i] == dst[i], "serialization/deserialization failed");
+        i += 1;
+    }
+}