diff --git a/tests/expected/dealloc/stack/expected b/tests/expected/dealloc/stack/expected
new file mode 100644
index 000000000000..1c56eb4366da
--- /dev/null
+++ b/tests/expected/dealloc/stack/expected
@@ -0,0 +1,4 @@
+Status: FAILURE\
+Description: "free argument must be dynamic object"
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/dealloc/stack/test.rs b/tests/expected/dealloc/stack/test.rs
new file mode 100644
index 000000000000..7d62e74d401d
--- /dev/null
+++ b/tests/expected/dealloc/stack/test.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use std::alloc::{dealloc, Layout};
+
+//! This test checks that Kani flags the deallocation of a stack-allocated
+//! variable
+
+#[kani::proof]
+fn check_dealloc_stack() {
+    let mut x = 6;
+    let layout = Layout::new::<i32>();
+    let p = &mut x as *mut i32;
+    unsafe {
+        dealloc(p as *mut u8, layout);
+    }
+}