diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
index b210b2c9333e..a871cd58f94f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::codegen_cprover_gotoc::{codegen::ty_stable::pointee_type_stable, GotocCtx};
 use crate::kani_middle::attributes::KaniAttributes;
 use cbmc::goto_program::FunctionContract;
 use cbmc::goto_program::{Expr, Lambda, Location, Type};
@@ -160,11 +160,17 @@ impl<'tcx> GotocCtx<'tcx> {
         let TyKind::RigidTy(RigidTy::Tuple(modifies_tys)) = modifies_ty.kind() else {
             unreachable!("found {:?}", modifies_ty.kind())
         };
+
+        for ty in &modifies_tys {
+            assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty);
+        }
+
         let assigns: Vec<_> = modifies_tys
             .into_iter()
+            // do not attempt to dereference (and assign) a ZST
+            .filter(|ty| !self.is_zst_stable(pointee_type_stable(*ty).unwrap()))
             .enumerate()
             .map(|(idx, ty)| {
-                assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty);
                 let ptr = modifies_args.clone().member(idx.to_string(), &self.symbol_table);
                 if self.is_fat_pointer_stable(ty) {
                     let unref = match ty.kind() {
diff --git a/tests/expected/function-contract/modifies/zst_pass.expected b/tests/expected/function-contract/modifies/zst_pass.expected
new file mode 100644
index 000000000000..ba2a8eb7decd
--- /dev/null
+++ b/tests/expected/function-contract/modifies/zst_pass.expected
@@ -0,0 +1,5 @@
+.assertion\
+- Status: SUCCESS\
+- Description: "ptr NULL or writable up to size"\
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/modifies/zst_pass.rs b/tests/expected/function-contract/modifies/zst_pass.rs
new file mode 100644
index 000000000000..89efd85a75f9
--- /dev/null
+++ b/tests/expected/function-contract/modifies/zst_pass.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::modifies(dst)]
+pub unsafe fn replace<T>(dst: *mut T, src: T) -> T {
+    std::ptr::replace(dst, src)
+}
+
+#[kani::proof_for_contract(replace)]
+pub fn check_replace_unit() {
+    check_replace_impl::<()>();
+}
+
+fn check_replace_impl<T: kani::Arbitrary + Eq + Clone>() {
+    let mut dst = T::any();
+    let orig = dst.clone();
+    let src = T::any();
+    let ret = unsafe { replace(&mut dst, src.clone()) };
+    assert_eq!(ret, orig);
+    assert_eq!(dst, src);
+}
diff --git a/tests/std-checks/core/mem.expected b/tests/std-checks/core/mem.expected
index 1484c83901fc..285a887307f8 100644
--- a/tests/std-checks/core/mem.expected
+++ b/tests/std-checks/core/mem.expected
@@ -1,7 +1,3 @@
 Checking harness mem::verify::check_swap_unit...
 
-Failed Checks: ptr NULL or writable up to size
-
-Summary:
-Verification failed for - mem::verify::check_swap_unit
-Complete - 6 successfully verified harnesses, 1 failures, 7 total.
+Complete - 7 successfully verified harnesses, 0 failures, 7 total.
diff --git a/tests/std-checks/core/ptr.expected b/tests/std-checks/core/ptr.expected
index 43d3bd6baf60..d6c2aff26442 100644
--- a/tests/std-checks/core/ptr.expected
+++ b/tests/std-checks/core/ptr.expected
@@ -1,4 +1,3 @@
 Summary:
-Verification failed for - ptr::verify::check_replace_unit
 Verification failed for - ptr::verify::check_as_ref_dangling
-Complete - 4 successfully verified harnesses, 2 failures, 6 total.
+Complete - 5 successfully verified harnesses, 1 failures, 6 total.
diff --git a/tests/std-checks/core/src/mem.rs b/tests/std-checks/core/src/mem.rs
index b0400d0a75f5..67b03d7a6188 100644
--- a/tests/std-checks/core/src/mem.rs
+++ b/tests/std-checks/core/src/mem.rs
@@ -48,8 +48,6 @@ mod verify {
         contracts::swap(&mut x, &mut y)
     }
 
-    /// FIX-ME: Modifies clause fail with pointer to ZST.
-    /// <https://github.com/model-checking/kani/issues/3181>
     #[kani::proof_for_contract(contracts::swap)]
     pub fn check_swap_unit() {
         let mut x: () = kani::any();
diff --git a/tests/std-checks/core/src/ptr.rs b/tests/std-checks/core/src/ptr.rs
index 49cf9e168214..1560889b56b3 100644
--- a/tests/std-checks/core/src/ptr.rs
+++ b/tests/std-checks/core/src/ptr.rs
@@ -89,8 +89,6 @@ mod verify {
         let _rf = unsafe { contracts::as_ref(&non_null) };
     }
 
-    /// FIX-ME: Modifies clause fail with pointer to ZST.
-    /// <https://github.com/model-checking/kani/issues/3181>
     #[kani::proof_for_contract(contracts::replace)]
     pub fn check_replace_unit() {
         check_replace_impl::<()>();