not sure if issue, more a question, is this expected or not: `--quiet` makes a failing verification run exit 0

[ivmat]

--quiet suppresses the failure exit code, not only the output. A run with a failing harness exits 0.

Reproduce

// quiet_probe.rs
#[kani::proof]
fn definitely_fails() {
    assert!(false, "must fail");
}

$ kani quiet_probe.rs > /dev/null; echo $?
1
$ kani quiet_probe.rs --quiet; echo $?
0

with Kani version: 0.67.0, built from main at d19941434.

Expected

Exit code 1 in both runs. --quiet's own help text promises it: "Produces no output, just an exit code and requested artifacts".

Root cause

print_final_summary returns early under --quiet (kani-driver/src/harness_runner.rs:294-296). The failure exit code is set at the end of the same function (std::process::exit(1), harness_runner.rs:363), and no other code path sets it. The early return skips it.

Related

#4731 records the zero-match instance of the same pattern: --quiet plus a filter typo exits 0, because that error also lives in print_final_summary (fixed by #4743). Found while preparing the two driver fixes from #4731.