diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
index 5f4610076bf1..e1b265751fd5 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
@@ -29,8 +29,17 @@ mod uninit_visitor;
 pub use ty_layout::{PointeeInfo, PointeeLayout};
 use uninit_visitor::{CheckUninitVisitor, InitRelevantInstruction, MemoryInitOp};
 
-const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] =
-    &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized"];
+// Function bodies of those functions will not be instrumented as not to cause infinite recursion.
+const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = &[
+    "KaniIsPtrInitialized",
+    "KaniSetPtrInitialized",
+    "KaniIsSliceChunkPtrInitialized",
+    "KaniSetSliceChunkPtrInitialized",
+    "KaniIsSlicePtrInitialized",
+    "KaniSetSlicePtrInitialized",
+    "KaniIsStrPtrInitialized",
+    "KaniSetStrPtrInitialized",
+];
 
 /// Instrument the code with checks for uninitialized memory.
 #[derive(Debug)]
@@ -164,10 +173,12 @@ impl UninitPass {
         };
 
         match operation {
-            MemoryInitOp::Check { .. } => {
+            MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::Check { .. } => {
                 self.build_get_and_check(tcx, body, source, operation, pointee_ty_info, skip_first)
             }
-            MemoryInitOp::Set { .. } | MemoryInitOp::SetRef { .. } => {
+            MemoryInitOp::SetSliceChunk { .. }
+            | MemoryInitOp::Set { .. }
+            | MemoryInitOp::SetRef { .. } => {
                 self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first)
             }
             MemoryInitOp::Unsupported { .. } => {
@@ -194,18 +205,34 @@ impl UninitPass {
         let ptr_operand = operation.mk_operand(body, source);
         match pointee_info.layout() {
             PointeeLayout::Sized { layout } => {
+                let layout_operand = mk_layout_operand(body, source, operation.position(), &layout);
+                // Depending on whether accessing the known number of elements in the slice, need to
+                // pass is as an argument.
+                let (diagnostic, args) = match &operation {
+                    MemoryInitOp::Check { .. } => {
+                        let diagnostic = "KaniIsPtrInitialized";
+                        let args = vec![ptr_operand.clone(), layout_operand];
+                        (diagnostic, args)
+                    }
+                    MemoryInitOp::CheckSliceChunk { .. } => {
+                        let diagnostic = "KaniIsSliceChunkPtrInitialized";
+                        let args =
+                            vec![ptr_operand.clone(), layout_operand, operation.expect_count()];
+                        (diagnostic, args)
+                    }
+                    _ => unreachable!(),
+                };
                 let is_ptr_initialized_instance = resolve_mem_init_fn(
-                    get_mem_init_fn_def(tcx, "KaniIsPtrInitialized", &mut self.mem_init_fn_cache),
+                    get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache),
                     layout.len(),
                     *pointee_info.ty(),
                 );
-                let layout_operand = mk_layout_operand(body, source, operation.position(), &layout);
                 collect_skipped(&operation, body, skip_first);
                 body.add_call(
                     &is_ptr_initialized_instance,
                     source,
                     operation.position(),
-                    vec![ptr_operand.clone(), layout_operand, operation.expect_count()],
+                    args,
                     ret_place.clone(),
                 );
             }
@@ -277,27 +304,50 @@ impl UninitPass {
 
         match pointee_info.layout() {
             PointeeLayout::Sized { layout } => {
+                let layout_operand = mk_layout_operand(body, source, operation.position(), &layout);
+                // Depending on whether writing to the known number of elements in the slice, need to
+                // pass is as an argument.
+                let (diagnostic, args) = match &operation {
+                    MemoryInitOp::Set { .. } | MemoryInitOp::SetRef { .. } => {
+                        let diagnostic = "KaniSetPtrInitialized";
+                        let args = vec![
+                            ptr_operand,
+                            layout_operand,
+                            Operand::Constant(ConstOperand {
+                                span: source.span(body.blocks()),
+                                user_ty: None,
+                                const_: MirConst::from_bool(value),
+                            }),
+                        ];
+                        (diagnostic, args)
+                    }
+                    MemoryInitOp::SetSliceChunk { .. } => {
+                        let diagnostic = "KaniSetSliceChunkPtrInitialized";
+                        let args = vec![
+                            ptr_operand,
+                            layout_operand,
+                            operation.expect_count(),
+                            Operand::Constant(ConstOperand {
+                                span: source.span(body.blocks()),
+                                user_ty: None,
+                                const_: MirConst::from_bool(value),
+                            }),
+                        ];
+                        (diagnostic, args)
+                    }
+                    _ => unreachable!(),
+                };
                 let set_ptr_initialized_instance = resolve_mem_init_fn(
-                    get_mem_init_fn_def(tcx, "KaniSetPtrInitialized", &mut self.mem_init_fn_cache),
+                    get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache),
                     layout.len(),
                     *pointee_info.ty(),
                 );
-                let layout_operand = mk_layout_operand(body, source, operation.position(), &layout);
                 collect_skipped(&operation, body, skip_first);
                 body.add_call(
                     &set_ptr_initialized_instance,
                     source,
                     operation.position(),
-                    vec![
-                        ptr_operand,
-                        layout_operand,
-                        operation.expect_count(),
-                        Operand::Constant(ConstOperand {
-                            span: source.span(body.blocks()),
-                            user_ty: None,
-                            const_: MirConst::from_bool(value),
-                        }),
-                    ],
+                    args,
                     ret_place,
                 );
             }
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
index 34befce23ce2..f4af8ee6e3b4 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
@@ -8,25 +8,31 @@ use stable_mir::mir::alloc::GlobalAlloc;
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::visit::{Location, PlaceContext};
 use stable_mir::mir::{
-    BasicBlockIdx, CastKind, ConstOperand, LocalDecl, MirVisitor, Mutability,
-    NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement,
-    StatementKind, Terminator, TerminatorKind,
+    BasicBlockIdx, CastKind, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand,
+    Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator,
+    TerminatorKind,
 };
-use stable_mir::ty::{ConstantKind, MirConst, RigidTy, Span, TyKind, UintTy};
+use stable_mir::ty::{ConstantKind, RigidTy, TyKind};
 use strum_macros::AsRefStr;
 
 /// Memory initialization operations: set or get memory initialization state for a given pointer.
 #[derive(AsRefStr, Clone, Debug)]
 pub enum MemoryInitOp {
+    /// Check memory initialization of data bytes in a memory region starting from the pointer
+    /// `operand` and of length `sizeof(operand)` bytes.
+    Check { operand: Operand },
+    /// Set memory initialization state of data bytes in a memory region starting from the pointer
+    /// `operand` and of length `sizeof(operand)` bytes.
+    Set { operand: Operand, value: bool, position: InsertPosition },
     /// Check memory initialization of data bytes in a memory region starting from the pointer
     /// `operand` and of length `count * sizeof(operand)` bytes.
-    Check { operand: Operand, count: Operand },
+    CheckSliceChunk { operand: Operand, count: Operand },
     /// Set memory initialization state of data bytes in a memory region starting from the pointer
     /// `operand` and of length `count * sizeof(operand)` bytes.
-    Set { operand: Operand, count: Operand, value: bool, position: InsertPosition },
+    SetSliceChunk { operand: Operand, count: Operand, value: bool, position: InsertPosition },
     /// Set memory initialization of data bytes in a memory region starting from the reference to
-    /// `operand` and of length `count * sizeof(operand)` bytes.
-    SetRef { operand: Operand, count: Operand, value: bool, position: InsertPosition },
+    /// `operand` and of length `sizeof(operand)` bytes.
+    SetRef { operand: Operand, value: bool, position: InsertPosition },
     /// Unsupported memory initialization operation.
     Unsupported { reason: String },
 }
@@ -37,9 +43,10 @@ impl MemoryInitOp {
     /// `MemoryInitOp::SetRef`.
     pub fn mk_operand(&self, body: &mut MutableBody, source: &mut SourceInstruction) -> Operand {
         match self {
-            MemoryInitOp::Check { operand, .. } | MemoryInitOp::Set { operand, .. } => {
-                operand.clone()
-            }
+            MemoryInitOp::Check { operand, .. }
+            | MemoryInitOp::Set { operand, .. }
+            | MemoryInitOp::CheckSliceChunk { operand, .. }
+            | MemoryInitOp::SetSliceChunk { operand, .. } => operand.clone(),
             MemoryInitOp::SetRef { operand, .. } => Operand::Copy(Place {
                 local: {
                     let place = match operand {
@@ -60,24 +67,34 @@ impl MemoryInitOp {
 
     pub fn expect_count(&self) -> Operand {
         match self {
-            MemoryInitOp::Check { count, .. }
-            | MemoryInitOp::Set { count, .. }
-            | MemoryInitOp::SetRef { count, .. } => count.clone(),
-            MemoryInitOp::Unsupported { .. } => unreachable!(),
+            MemoryInitOp::CheckSliceChunk { count, .. }
+            | MemoryInitOp::SetSliceChunk { count, .. } => count.clone(),
+            MemoryInitOp::Check { .. }
+            | MemoryInitOp::Set { .. }
+            | MemoryInitOp::SetRef { .. }
+            | MemoryInitOp::Unsupported { .. } => unreachable!(),
         }
     }
 
     pub fn expect_value(&self) -> bool {
         match self {
-            MemoryInitOp::Set { value, .. } | MemoryInitOp::SetRef { value, .. } => *value,
-            MemoryInitOp::Check { .. } | MemoryInitOp::Unsupported { .. } => unreachable!(),
+            MemoryInitOp::Set { value, .. }
+            | MemoryInitOp::SetSliceChunk { value, .. }
+            | MemoryInitOp::SetRef { value, .. } => *value,
+            MemoryInitOp::Check { .. }
+            | MemoryInitOp::CheckSliceChunk { .. }
+            | MemoryInitOp::Unsupported { .. } => unreachable!(),
         }
     }
 
     pub fn position(&self) -> InsertPosition {
         match self {
-            MemoryInitOp::Set { position, .. } | MemoryInitOp::SetRef { position, .. } => *position,
-            MemoryInitOp::Check { .. } | MemoryInitOp::Unsupported { .. } => InsertPosition::Before,
+            MemoryInitOp::Set { position, .. }
+            | MemoryInitOp::SetSliceChunk { position, .. }
+            | MemoryInitOp::SetRef { position, .. } => *position,
+            MemoryInitOp::Check { .. }
+            | MemoryInitOp::CheckSliceChunk { .. }
+            | MemoryInitOp::Unsupported { .. } => InsertPosition::Before,
         }
     }
 }
@@ -156,12 +173,12 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                 StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => {
                     self.super_statement(stmt, location);
                     // Source is a *const T and it must be initialized.
-                    self.push_target(MemoryInitOp::Check {
+                    self.push_target(MemoryInitOp::CheckSliceChunk {
                         operand: copy.src.clone(),
                         count: copy.count.clone(),
                     });
                     // Destimation is a *mut T so it gets initialized.
-                    self.push_target(MemoryInitOp::Set {
+                    self.push_target(MemoryInitOp::SetSliceChunk {
                         operand: copy.dst.clone(),
                         count: copy.count.clone(),
                         value: true,
@@ -186,7 +203,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                 {
                                     self.push_target(MemoryInitOp::Check {
                                         operand: Operand::Copy(place_to_add_projections.clone()),
-                                        count: mk_const_operand(1, location.span()),
                                     });
                                 };
                             }
@@ -195,7 +211,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                         if place_without_deref.ty(&self.locals).unwrap().kind().is_raw_ptr() {
                             self.push_target(MemoryInitOp::Set {
                                 operand: Operand::Copy(place_without_deref),
-                                count: mk_const_operand(1, location.span()),
                                 value: true,
                                 position: InsertPosition::After,
                             });
@@ -206,7 +221,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                         if let Rvalue::AddressOf(..) = rvalue {
                             self.push_target(MemoryInitOp::Set {
                                 operand: Operand::Copy(place.clone()),
-                                count: mk_const_operand(1, location.span()),
                                 value: true,
                                 position: InsertPosition::After,
                             });
@@ -217,7 +231,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                     self.super_statement(stmt, location);
                     self.push_target(MemoryInitOp::Set {
                         operand: Operand::Copy(place.clone()),
-                        count: mk_const_operand(1, location.span()),
                         value: false,
                         position: InsertPosition::After,
                     });
@@ -280,7 +293,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                     ));
                                     self.push_target(MemoryInitOp::Check {
                                         operand: args[0].clone(),
-                                        count: mk_const_operand(1, location.span()),
                                     });
                                 }
                                 "compare_bytes" => {
@@ -297,11 +309,11 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                         args[1].ty(self.locals).unwrap().kind(),
                                         TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
                                     ));
-                                    self.push_target(MemoryInitOp::Check {
+                                    self.push_target(MemoryInitOp::CheckSliceChunk {
                                         operand: args[0].clone(),
                                         count: args[2].clone(),
                                     });
-                                    self.push_target(MemoryInitOp::Check {
+                                    self.push_target(MemoryInitOp::CheckSliceChunk {
                                         operand: args[1].clone(),
                                         count: args[2].clone(),
                                     });
@@ -322,11 +334,11 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                         args[1].ty(self.locals).unwrap().kind(),
                                         TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
                                     ));
-                                    self.push_target(MemoryInitOp::Check {
+                                    self.push_target(MemoryInitOp::CheckSliceChunk {
                                         operand: args[0].clone(),
                                         count: args[2].clone(),
                                     });
-                                    self.push_target(MemoryInitOp::Set {
+                                    self.push_target(MemoryInitOp::SetSliceChunk {
                                         operand: args[1].clone(),
                                         count: args[2].clone(),
                                         value: true,
@@ -349,11 +361,9 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                     ));
                                     self.push_target(MemoryInitOp::Check {
                                         operand: args[0].clone(),
-                                        count: mk_const_operand(1, location.span()),
                                     });
                                     self.push_target(MemoryInitOp::Check {
                                         operand: args[1].clone(),
-                                        count: mk_const_operand(1, location.span()),
                                     });
                                 }
                                 "volatile_load" | "unaligned_volatile_load" => {
@@ -368,7 +378,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                     ));
                                     self.push_target(MemoryInitOp::Check {
                                         operand: args[0].clone(),
-                                        count: mk_const_operand(1, location.span()),
                                     });
                                 }
                                 "volatile_store" => {
@@ -383,7 +392,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                     ));
                                     self.push_target(MemoryInitOp::Set {
                                         operand: args[0].clone(),
-                                        count: mk_const_operand(1, location.span()),
                                         value: true,
                                         position: InsertPosition::After,
                                     });
@@ -398,7 +406,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                         args[0].ty(self.locals).unwrap().kind(),
                                         TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
                                     ));
-                                    self.push_target(MemoryInitOp::Set {
+                                    self.push_target(MemoryInitOp::SetSliceChunk {
                                         operand: args[0].clone(),
                                         count: args[2].clone(),
                                         value: true,
@@ -421,7 +429,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                     }
                                     "alloc::alloc::__rust_alloc_zeroed" => {
                                         /* Memory is initialized here, need to update shadow memory. */
-                                        self.push_target(MemoryInitOp::Set {
+                                        self.push_target(MemoryInitOp::SetSliceChunk {
                                             operand: Operand::Copy(destination.clone()),
                                             count: args[0].clone(),
                                             value: true,
@@ -430,7 +438,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                     }
                                     "alloc::alloc::__rust_dealloc" => {
                                         /* Memory is uninitialized here, need to update shadow memory. */
-                                        self.push_target(MemoryInitOp::Set {
+                                        self.push_target(MemoryInitOp::SetSliceChunk {
                                             operand: args[0].clone(),
                                             count: args[1].clone(),
                                             value: false,
@@ -461,7 +469,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                         RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => {
                             self.push_target(MemoryInitOp::SetRef {
                                 operand: Operand::Copy(place.clone()),
-                                count: mk_const_operand(1, location.span()),
                                 value: true,
                                 position: InsertPosition::Before,
                             });
@@ -472,7 +479,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                     if place_ty.kind().is_raw_ptr() {
                         self.push_target(MemoryInitOp::Set {
                             operand: Operand::Copy(place.clone()),
-                            count: mk_const_operand(1, location.span()),
                             value: false,
                             position: InsertPosition::After,
                         });
@@ -500,7 +506,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                     if ptr_ty.kind().is_raw_ptr() {
                         self.push_target(MemoryInitOp::Check {
                             operand: Operand::Copy(intermediate_place.clone()),
-                            count: mk_const_operand(1, location.span()),
                         });
                     }
                 }
@@ -535,7 +540,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                             // If a static is a raw pointer, need to mark it as initialized.
                             self.push_target(MemoryInitOp::Set {
                                 operand: Operand::Constant(constant.clone()),
-                                count: mk_const_operand(1, location.span()),
                                 value: true,
                                 position: InsertPosition::Before,
                             });
@@ -696,15 +700,6 @@ fn can_skip_intrinsic(intrinsic_name: &str) -> bool {
     }
 }
 
-/// Create a constant operand with a given value and span.
-fn mk_const_operand(value: usize, span: Span) -> Operand {
-    Operand::Constant(ConstOperand {
-        span,
-        user_ty: None,
-        const_: MirConst::try_from_uint(value as u128, UintTy::Usize).unwrap(),
-    })
-}
-
 /// Try removing a topmost deref projection from a place if it exists, returning a place without it.
 fn try_remove_topmost_deref(place: &Place) -> Option<Place> {
     let mut new_place = place.clone();
diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
index ea7bf8625228..c4534bf11b4d 100644
--- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
@@ -216,11 +216,7 @@ impl IntrinsicGeneratorPass {
                             &is_ptr_initialized_instance,
                             &mut terminator,
                             InsertPosition::Before,
-                            vec![
-                                Operand::Copy(Place::from(1)),
-                                layout_operand,
-                                Operand::Copy(Place::from(2)),
-                            ],
+                            vec![Operand::Copy(Place::from(1)), layout_operand],
                             Place::from(ret_var),
                         );
                     }
diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
index 201d027124d0..be6a80ee0fe2 100644
--- a/library/kani/src/mem.rs
+++ b/library/kani/src/mem.rs
@@ -300,16 +300,13 @@ unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
 /// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
 #[rustc_diagnostic_item = "KaniIsInitialized"]
 #[inline(never)]
-pub fn is_initialized<T: ?Sized>(_ptr: *const T, _len: usize) -> bool {
+pub fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
     kani_intrinsic()
 }
 
 /// A helper to to assert `is_initialized` to use it as a part of other predicates.
 fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
-    crate::assert(
-        is_initialized(ptr, 1),
-        "Undefined Behavior: Reading from an uninitialized pointer",
-    );
+    crate::assert(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer");
     true
 }
 
diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs
index b05fb2a60308..a09e515d7e17 100644
--- a/library/kani/src/mem_init.rs
+++ b/library/kani/src/mem_init.rs
@@ -44,13 +44,58 @@ impl MemoryInitializationState {
         Self { tracked_object_id: 0, tracked_offset: 0, value: false }
     }
 
+    /// Return currently tracked memory initialization state if `ptr` points to the currently
+    /// tracked object and the tracked offset lies within `LAYOUT_SIZE` bytes of `ptr`. Return
+    /// `true` otherwise.
+    ///
+    /// Such definition is necessary since both tracked object and tracked offset are chosen
+    /// non-deterministically.
+    pub fn get<const LAYOUT_SIZE: usize>(
+        &mut self,
+        ptr: *const u8,
+        layout: Layout<LAYOUT_SIZE>,
+    ) -> bool {
+        let obj = crate::mem::pointer_object(ptr);
+        let offset = crate::mem::pointer_offset(ptr);
+        if self.tracked_object_id == obj
+            && self.tracked_offset >= offset
+            && self.tracked_offset < offset + LAYOUT_SIZE
+        {
+            !layout[(self.tracked_offset - offset) % LAYOUT_SIZE] || self.value
+        } else {
+            true
+        }
+    }
+
+    /// Set currently tracked memory initialization state if `ptr` points to the currently tracked
+    /// object and the tracked offset lies within `LAYOUT_SIZE` bytes of `ptr`. Do nothing
+    /// otherwise.
+    ///
+    /// Such definition is necessary since both tracked object and tracked offset are chosen
+    /// non-deterministically.
+    pub fn set<const LAYOUT_SIZE: usize>(
+        &mut self,
+        ptr: *const u8,
+        layout: Layout<LAYOUT_SIZE>,
+        value: bool,
+    ) {
+        let obj = crate::mem::pointer_object(ptr);
+        let offset = crate::mem::pointer_offset(ptr);
+        if self.tracked_object_id == obj
+            && self.tracked_offset >= offset
+            && self.tracked_offset < offset + LAYOUT_SIZE
+        {
+            self.value = layout[(self.tracked_offset - offset) % LAYOUT_SIZE] && value;
+        }
+    }
+
     /// Return currently tracked memory initialization state if `ptr` points to the currently
     /// tracked object and the tracked offset lies within `LAYOUT_SIZE * num_elts` bytes of `ptr`.
     /// Return `true` otherwise.
     ///
     /// Such definition is necessary since both tracked object and tracked offset are chosen
     /// non-deterministically.
-    pub fn get<const LAYOUT_SIZE: usize>(
+    pub fn get_slice<const LAYOUT_SIZE: usize>(
         &mut self,
         ptr: *const u8,
         layout: Layout<LAYOUT_SIZE>,
@@ -74,7 +119,7 @@ impl MemoryInitializationState {
     ///
     /// Such definition is necessary since both tracked object and tracked offset are chosen
     /// non-deterministically.
-    pub fn set<const LAYOUT_SIZE: usize>(
+    pub fn set_slice<const LAYOUT_SIZE: usize>(
         &mut self,
         ptr: *const u8,
         layout: Layout<LAYOUT_SIZE>,
@@ -107,55 +152,63 @@ fn initialize_memory_initialization_state() {
 }
 
 /// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`.
-#[rustc_diagnostic_item = "KaniIsUnitPtrInitialized"]
-fn is_unit_ptr_initialized<const LAYOUT_SIZE: usize>(
-    ptr: *const (),
+#[rustc_diagnostic_item = "KaniIsPtrInitialized"]
+fn is_ptr_initialized<const LAYOUT_SIZE: usize, T>(
+    ptr: *const T,
     layout: Layout<LAYOUT_SIZE>,
-    num_elts: usize,
 ) -> bool {
     if LAYOUT_SIZE == 0 {
         return true;
     }
-    unsafe { MEM_INIT_STATE.get(ptr as *const u8, layout, num_elts) }
+    let (ptr, _) = ptr.to_raw_parts();
+    unsafe { MEM_INIT_STATE.get(ptr as *const u8, layout) }
 }
 
 /// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`.
-#[rustc_diagnostic_item = "KaniSetUnitPtrInitialized"]
-fn set_unit_ptr_initialized<const LAYOUT_SIZE: usize>(
-    ptr: *const (),
+#[rustc_diagnostic_item = "KaniSetPtrInitialized"]
+fn set_ptr_initialized<const LAYOUT_SIZE: usize, T>(
+    ptr: *const T,
     layout: Layout<LAYOUT_SIZE>,
-    num_elts: usize,
     value: bool,
 ) {
     if LAYOUT_SIZE == 0 {
         return;
     }
+    let (ptr, _) = ptr.to_raw_parts();
     unsafe {
-        MEM_INIT_STATE.set(ptr as *const u8, layout, num_elts, value);
+        MEM_INIT_STATE.set(ptr as *const u8, layout, value);
     }
 }
 
 /// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`.
-#[rustc_diagnostic_item = "KaniIsPtrInitialized"]
-fn is_ptr_initialized<const LAYOUT_SIZE: usize, T>(
+#[rustc_diagnostic_item = "KaniIsSliceChunkPtrInitialized"]
+fn is_slice_chunk_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     ptr: *const T,
     layout: Layout<LAYOUT_SIZE>,
     num_elts: usize,
 ) -> bool {
+    if LAYOUT_SIZE == 0 {
+        return true;
+    }
     let (ptr, _) = ptr.to_raw_parts();
-    is_unit_ptr_initialized(ptr, layout, num_elts)
+    unsafe { MEM_INIT_STATE.get_slice(ptr as *const u8, layout, num_elts) }
 }
 
 /// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`.
-#[rustc_diagnostic_item = "KaniSetPtrInitialized"]
-fn set_ptr_initialized<const LAYOUT_SIZE: usize, T>(
+#[rustc_diagnostic_item = "KaniSetSliceChunkPtrInitialized"]
+fn set_slice_chunk_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     ptr: *const T,
     layout: Layout<LAYOUT_SIZE>,
     num_elts: usize,
     value: bool,
 ) {
+    if LAYOUT_SIZE == 0 {
+        return;
+    }
     let (ptr, _) = ptr.to_raw_parts();
-    set_unit_ptr_initialized(ptr, layout, num_elts, value);
+    unsafe {
+        MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value);
+    }
 }
 
 /// Get initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr`.
@@ -164,8 +217,11 @@ fn is_slice_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     ptr: *const [T],
     layout: Layout<LAYOUT_SIZE>,
 ) -> bool {
+    if LAYOUT_SIZE == 0 {
+        return true;
+    }
     let (ptr, num_elts) = ptr.to_raw_parts();
-    is_unit_ptr_initialized(ptr, layout, num_elts)
+    unsafe { MEM_INIT_STATE.get_slice(ptr as *const u8, layout, num_elts) }
 }
 
 /// Set initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`.
@@ -175,8 +231,13 @@ fn set_slice_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     layout: Layout<LAYOUT_SIZE>,
     value: bool,
 ) {
+    if LAYOUT_SIZE == 0 {
+        return;
+    }
     let (ptr, num_elts) = ptr.to_raw_parts();
-    set_unit_ptr_initialized(ptr, layout, num_elts, value);
+    unsafe {
+        MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value);
+    }
 }
 
 /// Get initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr`.
@@ -185,8 +246,11 @@ fn is_str_ptr_initialized<const LAYOUT_SIZE: usize>(
     ptr: *const str,
     layout: Layout<LAYOUT_SIZE>,
 ) -> bool {
+    if LAYOUT_SIZE == 0 {
+        return true;
+    }
     let (ptr, num_elts) = ptr.to_raw_parts();
-    is_unit_ptr_initialized(ptr, layout, num_elts)
+    unsafe { MEM_INIT_STATE.get_slice(ptr as *const u8, layout, num_elts) }
 }
 
 /// Set initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`.
@@ -196,6 +260,11 @@ fn set_str_ptr_initialized<const LAYOUT_SIZE: usize>(
     layout: Layout<LAYOUT_SIZE>,
     value: bool,
 ) {
+    if LAYOUT_SIZE == 0 {
+        return;
+    }
     let (ptr, num_elts) = ptr.to_raw_parts();
-    set_unit_ptr_initialized(ptr, layout, num_elts, value);
+    unsafe {
+        MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value);
+    }
 }
diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
index de6c535be8dc..74061d07404b 100644
--- a/library/kani_core/src/mem.rs
+++ b/library/kani_core/src/mem.rs
@@ -306,14 +306,14 @@ macro_rules! kani_mem {
         /// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
         #[rustc_diagnostic_item = "KaniIsInitialized"]
         #[inline(never)]
-        pub fn is_initialized<T: ?Sized>(_ptr: *const T, _len: usize) -> bool {
+        pub fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
             kani_intrinsic()
         }
 
         /// A helper to to assert `is_initialized` to use it as a part of other predicates.
         fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
             assert!(
-                is_initialized(ptr, 1),
+                is_initialized(ptr),
                 "Undefined Behavior: Reading from an uninitialized pointer",
             );
             true