diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs
index ad4392de7c1b..711b9b005624 100644
--- a/library/kani/src/concrete_playback.rs
+++ b/library/kani/src/concrete_playback.rs
@@ -40,7 +40,9 @@ pub fn concrete_playback_run<F: Fn()>(mut local_concrete_vals: Vec<Vec<u8>>, pro
     });
 }
 
-/// Concrete playback implementation of kani::any_raw_internal.
+/// Concrete playback implementation of
+/// kani::any_raw_internal. Because CBMC does not bother putting in
+/// Zero-Sized Types, those are defaulted to an empty vector.
 ///
 /// # Safety
 ///
@@ -49,7 +51,11 @@ pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
     let mut next_concrete_val: Vec<u8> = Vec::new();
     CONCRETE_VALS.with(|glob_concrete_vals| {
         let mut_ref_glob_concrete_vals = &mut *glob_concrete_vals.borrow_mut();
-        next_concrete_val = mut_ref_glob_concrete_vals.pop().expect("Not enough det vals found");
+        next_concrete_val = if SIZE_T > 0 {
+            mut_ref_glob_concrete_vals.pop().expect("Not enough det vals found")
+        } else {
+            vec![]
+        };
     });
     let next_concrete_val_len = next_concrete_val.len();
     let bytes_t: [u8; SIZE_T] = next_concrete_val.try_into().expect(&format!(
diff --git a/tests/script-based-pre/playback_zero_size/config.yml b/tests/script-based-pre/playback_zero_size/config.yml
new file mode 100644
index 000000000000..4f9347ff4b7b
--- /dev/null
+++ b/tests/script-based-pre/playback_zero_size/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: playback_zst.sh
+expected: playback_zst.expected
diff --git a/tests/script-based-pre/playback_zero_size/original.rs b/tests/script-based-pre/playback_zero_size/original.rs
new file mode 100644
index 000000000000..a1c562599709
--- /dev/null
+++ b/tests/script-based-pre/playback_zero_size/original.rs
@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This checks that Kani zero-size playback, 2 of them in a row.
+
+#[kani::proof]
+fn any_is_ok() {
+    let unit: () = kani::any();
+    kani::cover!(unit == ());
+}
diff --git a/tests/script-based-pre/playback_zero_size/playback_zst.expected b/tests/script-based-pre/playback_zero_size/playback_zst.expected
new file mode 100644
index 000000000000..d809e2fda5e1
--- /dev/null
+++ b/tests/script-based-pre/playback_zero_size/playback_zst.expected
@@ -0,0 +1,5 @@
+[TEST] Generate test...
+Checking harness any_is_ok
+
+[TEST] Run test...
+test result: ok. 1 passed; 0 failed;
diff --git a/tests/script-based-pre/playback_zero_size/playback_zst.sh b/tests/script-based-pre/playback_zero_size/playback_zst.sh
new file mode 100755
index 000000000000..7c8a23ab9643
--- /dev/null
+++ b/tests/script-based-pre/playback_zero_size/playback_zst.sh
@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+# Test that concrete playback -Z concrete-playback executes as expected
+set -o pipefail
+set -o nounset
+
+RS_FILE="modified.rs"
+cp original.rs ${RS_FILE}
+
+echo "[TEST] Generate test..."
+kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace
+
+echo "[TEST] Run test..."
+kani playback -Z concrete-playback ${RS_FILE} -- kani_concrete_playback
+
+# Cleanup
+rm ${RS_FILE}