Requested feature: Only included FAILED properties in the failure pop-up
Use case: Debugging a harness failure
Link to relevant documentation (Rust reference, Nomicon, RFC):
Test case:
/// The unwind value is too low triggering a unwind failure. This will flip all properties to undetermined.
#[kani::proof]
#[kani::unwind(1)]
fn verify_unwrap() {
let mut option: Option<&str> = Some("hi");
for i in 0..2 {
if i % 2 == 0 {
option = None;
}
}
option.unwrap();
}
For this test, the harness failure popup will be quite verbose since it will include all properties that were marked with UNDETERMINED.