Concrete playback should support all kind of property failures

[celinval]

Requested feature: Concrete playback should generate tests for all kind of failures, even those that trigger a UB.
Use case: Users wanting to debug a failure that is not related to a user assertion, such as invalid memory access, could run the generated test case under valgrind or miri to detect the issue.
Link to relevant documentation (Rust reference, Nomicon, RFC):

Dummy test case:

#[kani::proof]
fn check_len() {
    let mut input = vec!['h', 't'];
    let new_len = kani::any();
    unsafe { input.set_len(new_len) };
    let last = input.pop();
    assert_eq!(last.unwrap(), 't');
}

This test should generate at least 3 different tests. One for our of bound access (e.g.: new_len = 10), one for unwrap() a none object (new_len = 0), and one for the assertion failure (new_len = 1).

For the out of bounds case, the test would likely succeed in a regular execution, but it would fail when running it with MIRI or valgrind.

Note: Since these failures might not be so trivial, we may want a different structure or name schema for them to differentiate from things that should fail in a simple execution.