Kani cannot verify bolero harness after concrete test has been added

[celinval]

I tried this code:

#[cfg(test)]
mod bolero_harness {
    #[test]
    #[cfg_attr(kani, kani::proof)]
    fn dummy_harness() {
        bolero::check!()
            .with_type()
            .cloned()
            .for_each(|(a, b): (u8, u8)| assert!(a < b || a > b));
    }
}

using the following command line sequence:

cargo kani --tests -Z concrete-playback --concrete-playback=inplace
cargo kani --tests

with Kani version:

I expected to see this happen: Both commands should succeed

Instead, this happened: The second command failed due to a compilation error

error[E0425]: cannot find function `concrete_playback_run` in crate `kani`
  --> src/lib.rs:
   |
   |         kani::concrete_playback_run(concrete_vals, fuzz_add);
   |               ^^^^^^^^^^^^^^^^^^^^^ not found in `kani`

The problem is that the harness uses a function that is only included when we execute concrete playback. We should still implement that function in verification mode.