Delay printing playback harness until after verification status (#2480)

kani-driver/src/call_cbmc.rs

@@ -66,8 +66,7 @@ impl KaniSession {
 
         let start_time = Instant::now();
 
-        let mut verification_results = if self.args.output_format == crate::args::OutputFormat::Old
-        {
+        let verification_results = if self.args.output_format == crate::args::OutputFormat::Old {
             if self.run_terminal(cmd).is_err() {
                 VerificationResult::mock_failure()
             } else {
@@ -93,7 +92,6 @@ impl KaniSession {
             VerificationResult::from(output, harness.attributes.should_panic, start_time)
         };
 
-        self.gen_and_add_concrete_playback(harness, &mut verification_results)?;
         Ok(verification_results)
     }
 

kani-driver/src/harness_runner.rs

@@ -89,7 +89,7 @@ impl KaniSession {
             // Strictly speaking, we're faking success here. This is more "no error"
             Ok(VerificationResult::mock_success())
         } else {
-            let result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
+            let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
 
             // When quiet, we don't want to print anything at all.
             // When output is old, we also don't have real results to print.
@@ -99,7 +99,7 @@ impl KaniSession {
                     result.render(&self.args.output_format, harness.attributes.should_panic)
                 );
             }
-
+            self.gen_and_add_concrete_playback(harness, &mut result)?;
             Ok(result)
         }
     }

tests/ui/concrete-playback/message-order/expected

@@ -0,0 +1,14 @@
+VERIFICATION:- SUCCESSFUL
+
+
+Concrete playback unit test for `dummy`:
+```
+#[test]
+fn kani_concrete_playback_dummy
+    let concrete_vals: Vec<Vec<u8>> = vec![
+        // 32778
+        vec![10, 128, 0, 0],
+    ];
+    kani::concrete_playback_run(concrete_vals, dummy);
+}
+```

tests/ui/concrete-playback/message-order/main.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --concrete-playback=print --harness dummy -Z concrete-playback
+
+#[kani::proof]
+fn dummy() {
+    kani::cover!(kani::any::<u32>() != 10);
+}