Test cases.

tests/script-based-pre/zero-size/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: playback_opts.sh
+expected: playback_opts.expected

tests/script-based-pre/zero-size/original.rs

@@ -0,0 +1,11 @@
+// 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();
+    let unit2: () = kani::any();
+    kani::cover!(unit == ());
+    kani::cover!(unit2 == ());
+}

tests/script-based-pre/zero-size/playback_opts.expected

@@ -0,0 +1,5 @@
+[TEST] Generate test...
+Checking harness any_is_ok
+
+[TEST] Run test...
+test result: ok. 1 passed; 0 failed;

tests/script-based-pre/zero-size/playback_opts.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}