diff --git a/tests/cargo-kani/storage-markers/Cargo.toml b/tests/cargo-kani/storage-markers/Cargo.toml
new file mode 100644
index 000000000000..cb98b6df5835
--- /dev/null
+++ b/tests/cargo-kani/storage-markers/Cargo.toml
@@ -0,0 +1,5 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[workspace]
+members = ["crate-with-bug", "crate-with-harness"]
+resolver = "2"
diff --git a/tests/cargo-kani/storage-markers/crate-with-bug/Cargo.toml b/tests/cargo-kani/storage-markers/crate-with-bug/Cargo.toml
new file mode 100644
index 000000000000..3cec8dac16b0
--- /dev/null
+++ b/tests/cargo-kani/storage-markers/crate-with-bug/Cargo.toml
@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "crate-with-bug"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
diff --git a/tests/cargo-kani/storage-markers/crate-with-bug/src/lib.rs b/tests/cargo-kani/storage-markers/crate-with-bug/src/lib.rs
new file mode 100644
index 000000000000..3e6967bdbfe4
--- /dev/null
+++ b/tests/cargo-kani/storage-markers/crate-with-bug/src/lib.rs
@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This function contains a use-after-free bug.
+
+pub fn fn_with_bug() -> i32 {
+    let raw_ptr = {
+        let var = 10;
+        &var as *const i32
+    };
+    unsafe { *raw_ptr }
+}
diff --git a/tests/cargo-kani/storage-markers/crate-with-harness/Cargo.toml b/tests/cargo-kani/storage-markers/crate-with-harness/Cargo.toml
new file mode 100644
index 000000000000..7cfe7126d845
--- /dev/null
+++ b/tests/cargo-kani/storage-markers/crate-with-harness/Cargo.toml
@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "crate-with-harness"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+crate-with-bug = { path = "../crate-with-bug" }
diff --git a/tests/cargo-kani/storage-markers/crate-with-harness/call_fn_with_bug.expected b/tests/cargo-kani/storage-markers/crate-with-harness/call_fn_with_bug.expected
new file mode 100644
index 000000000000..68ef53cc06ec
--- /dev/null
+++ b/tests/cargo-kani/storage-markers/crate-with-harness/call_fn_with_bug.expected
@@ -0,0 +1,3 @@
+Status: FAILURE\
+Description: "dereference failure: dead object"\
+in function crate_with_bug::fn_with_bug
diff --git a/tests/cargo-kani/storage-markers/crate-with-harness/src/lib.rs b/tests/cargo-kani/storage-markers/crate-with-harness/src/lib.rs
new file mode 100644
index 000000000000..a44cfaf976be
--- /dev/null
+++ b/tests/cargo-kani/storage-markers/crate-with-harness/src/lib.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that Kani captures the case of a use-after-free issue as
+// described in https://github.com/model-checking/kani/issues/3061 even across
+// crates. The test calls a function from another crate that has the bug.
+
+#[kani::proof]
+pub fn call_fn_with_bug() {
+    let _x = crate_with_bug::fn_with_bug();
+}