2 Zero-size types result in a harness with the same name

[YoshikiTakashima]

I tried this code:

//!file.rs

//! 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 == ());
}

using the following command line invocation:

kani file.rs -Z concrete-playback --concrete-playback=inplace
kani playback -Z concrete-playback file.rs -- kani_concrete_playback

with Kani version:

I expected to see this happen: I expected 2 independently named harnesses to be injected.

Instead, this happened: the 2 harnesses have the same name. Probably
because we did not move in the index.

After discussion, we should Inject 1 harness deduplicated.

[YoshikiTakashima]

This should've been caught in #2496, but was not.

[celinval]

Why do you expect two different harnesses?