Fix exit code swallowed by --quiet on verification failure

[rbeauchamp]

Description

kani --quiet (and cargo kani --quiet) always exits 0, even when verification fails. print_final_summary in kani-driver/src/harness_runner.rs returned Ok(()) early under --quiet, skipping the process::exit(1) path used in non-quiet mode. This silently breaks CI pipelines that rely on the exit code while suppressing output.

The fix hoists the failure/success partitions (and the autoharness failing count) above the quiet gate so the exit status is computed the same way in both modes. The quiet-mode contract — no verification output on stdout — is preserved; only the exit code changes (0 → 1 on failure).

Context

Reported by @ivmat in #4745: running kani --quiet on a failing harness prints nothing (correct) but returns exit status 0 (incorrect), so failures are invisible to scripts and CI.

Manual testing

New script-based regression test tests/script-based-pre/quiet-exit-code/: runs kani --quiet on a failing and a passing harness and asserts (a) exit code 1 / 0 respectively, and (b) empty stdout/stderr in both cases. Verified RED without the fix (exit 0 on failure) and GREEN with it, on this branch. cargo test -p kani-driver passes (101/101).

Resolves #4745

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

Thanks @rbeauchamp. This PR looks like a duplicate of #4771 tho

[rbeauchamp]

Thanks for pointing this out, @celinval—I missed #4771. I’m closing this duplicate in favor of #4771, which is already under review. Thanks @ivmat for the fix!