diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index 9e785910ea0f..56b7da2e7628 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -11,7 +11,7 @@ use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
-use cbmc::goto_program::{Expr, ExprValue, Location, Type};
+use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{TagEncoding, Variants};
@@ -636,6 +636,14 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    fn is_zst_object(&self, expr: &Expr) -> bool {
+        match expr.value() {
+            ExprValue::Symbol { .. } => expr.typ().sizeof(&self.symbol_table) == 0,
+            ExprValue::Member { lhs, .. } => self.is_zst_object(lhs),
+            _ => false,
+        }
+    }
+
     /// Codegen the reference to a given place.
     /// We currently have a somewhat weird way of handling ZST.
     /// - For `*(&T)` where `T: Unsized`, the projection's `goto_expr` is a thin pointer, so we
@@ -647,25 +655,28 @@ impl<'tcx> GotocCtx<'tcx> {
         let projection =
             unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place));
         if self.use_thin_pointer_stable(place_ty) {
-            // For ZST objects rustc does not necessarily generate individual objects.
-            let need_not_be_unique = match projection.goto_expr.value() {
-                ExprValue::Symbol { .. } => self.is_zst_stable(place_ty),
-                _ => false,
-            };
-            let address_of = projection.goto_expr.address_of();
-            if need_not_be_unique {
-                let global_zst_name = "__kani_zst_object";
-                let zst_typ = self.codegen_ty_stable(place_ty);
-                let global_zst_object = self.ensure_global_var(
-                    global_zst_name,
-                    false,
-                    zst_typ,
-                    Location::none(),
-                    |_, _| None, // zero-sized, so no initialization necessary
+            // For ZST objects rustc does not necessarily generate any actual objects.
+            let need_not_be_an_object = self.is_zst_object(&projection.goto_expr);
+            let address_of = projection.goto_expr.clone().address_of();
+            if need_not_be_an_object {
+                // Create a non-deterministic numeric value, assume it is non-zero and (when
+                // interpreted as an address) of proper alignment for the type, and cast that
+                // numeric value to a pointer type.
+                let loc = projection.goto_expr.location();
+                let (var, decl) =
+                    self.decl_temp_variable(Type::size_t(), Some(Type::size_t().nondet()), *loc);
+                let assume_non_zero =
+                    Stmt::assume(var.clone().neq(Expr::int_constant(0, var.typ().clone())), *loc);
+                let layout = self.layout_of_stable(place_ty);
+                let alignment = Expr::int_constant(layout.align.abi.bytes(), var.typ().clone());
+                let assume_aligned = Stmt::assume(
+                    var.clone().rem(alignment).eq(Expr::int_constant(0, var.typ().clone())),
+                    *loc,
                 );
-                Type::bool().nondet().ternary(
-                    address_of.clone(),
-                    global_zst_object.address_of().cast_to(address_of.typ().clone()),
+                let cast_to_pointer_type = var.cast_to(address_of.typ().clone()).as_stmt(*loc);
+                Expr::statement_expression(
+                    vec![decl, assume_non_zero, assume_aligned, cast_to_pointer_type],
+                    address_of.typ().clone(),
                 )
             } else {
                 // Just return the address of the place dereferenced.
diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
index 43062ebed6a1..704b6ebadd4d 100644
--- a/library/kani/src/mem.rs
+++ b/library/kani/src/mem.rs
@@ -61,25 +61,16 @@ where
     crate::assert(!ptr.is_null(), "Expected valid pointer, but found `null`");
 
     let (thin_ptr, metadata) = ptr.to_raw_parts();
-    can_read(&metadata, thin_ptr)
-}
-
-fn can_read<M, T>(metadata: &M, data_ptr: *const ()) -> bool
-where
-    M: PtrProperties<T>,
-    T: ?Sized,
-{
-    let marker = Internal;
-    let sz = metadata.pointee_size(marker);
-    if metadata.dangling(marker) as *const _ == data_ptr {
-        crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access")
+    let sz = metadata.pointee_size(Internal);
+    if sz == 0 {
+        true // ZST pointers are always valid
     } else {
         crate::assert(
-            is_read_ok(data_ptr, sz),
+            is_read_ok(thin_ptr, sz),
             "Expected valid pointer, but found dangling pointer",
         );
+        true
     }
-    true
 }
 
 mod private {
@@ -257,13 +248,13 @@ mod tests {
     }
 
     #[test]
-    #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")]
+    #[should_panic(expected = "Expected valid pointer, but found dangling pointer")]
     fn test_dangling_char() {
         test_dangling_of_t::<char>();
     }
 
     #[test]
-    #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")]
+    #[should_panic(expected = "Expected valid pointer, but found dangling pointer")]
     fn test_dangling_slice() {
         test_dangling_of_t::<&str>();
     }