kani: A case where concrete values in trace/playback do not trigger an assertion violation

I tried this code:

#[derive(Debug)]
pub struct Data {
    pub _type: Type,
    pub array: [u8; MAX_ARRAY_LENGTH],
}

impl Data {
    fn is_valid(&self) -> bool {
        (self.array.len() == MAX_ARRAY_LENGTH)
            && ((self._type == Type::Apple) || (self._type == Type::Banana))
    }

    pub fn set_array(&mut self, idx: usize, array: [u8; 4]) -> Result<(), &str> {
        if idx >= MAX_U32_DATA_IDX {
            return Err("invalid input");
        }
        let start = idx * core::mem::size_of::<u32>();
        let end = start + core::mem::size_of::<u32>();
        self.array[start..end].copy_from_slice(&array);
        Ok(())
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
#[repr(u8)]
pub enum Type {
    Apple = 0,
    Banana = 1,
}

const MAX_ARRAY_LENGTH: usize = 8;
const MAX_U32_DATA_IDX: usize = 2;

#[kani::proof]
fn proof_harness() {
    let mut data = Data {
        _type: Type::Apple,
        array: [0; MAX_ARRAY_LENGTH],
    };
    let index = kani::any();
    let param = kani::any();
    let res = data.set_array(index, param);
    if let Ok(v) = res {
        assert!(data.is_valid());            // this point makes the verification fail, as `_type` field 
                                             // contain an unexpected value for some reasons
    }
}

fn main() {}

using the following command line invocation:

cargo kani --enable-unstable --concrete-playback=inplace
cargo test

with Kani version: 0.14.1, 0.15.0 (3c7e3fc9)

I expected to see this happen: I think that the verification should be successful, but it failed. If the verification has failed and concrete values have been generated with playback, using it should trigger the assertion violation like the below (I also have used the values in --visualize, but it does not trigger the assertion violation too.).

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s

Instead, this happened:

The result for cargo kani

SUMMARY:
 ** 1 of 203 failed (2 unreachable)
Failed Checks: assertion failed: data.is_valid()
 File: "/home/xxx/test/kani-test/data/src/main.rs", line 44, in proof_harness

VERIFICATION:- FAILED
Verification Time: 0.53910637s

The result for cargo test with the generated concrete values

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s

cargo test used the following genereted code

#[test]
fn kani_concrete_playback_proof_harness_8995903321428480627() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 1ul
        vec![1, 0, 0, 0, 0, 0, 0, 0],
        // 0
        vec![0],
        // 10
        vec![10],
        // 0
        vec![0],
        // 0
        vec![0],
    ];
    kani::concrete_playback_run(concrete_vals, proof_harness);
}