Keep completed results when --fail-fast aborts a run

[ivmat]

check_all_harnesses collected results with collect::<Result<Vec<_>>>(), which short-circuits on the first error. A --fail-fast abort was such an error, so every result that had already completed was dropped. The summary then contradicted the per-harness output above it, and --export-json under-reported the run the same way.

Completed results now accumulate in a shared vector as harnesses finish. The abort signal carries no payload; the failing harness records its result like any other. Results are re-sorted into harness order after the parallel loop, since completion order is nondeterministic.

The parallel fail-fast UI test pinned the old behavior: "1 failures, 1 total" for ten failing harnesses under --jobs 4. With completed results retained, those counts depend on thread scheduling, so the test becomes a script-based test asserting the stable properties: the run aborts early (fewer than ten run) and every counted harness is a failure. The sequential UI test is unchanged: it aborts on its first harness, so its pinned summary stays correct. A new sequential script-based test proves retention deterministically ("1 successfully verified, 1 failures, 2 total"); it fails on main.

Testing: cargo test -p kani-driver, rustfmt, and clippy are clean; the two new script-based tests and the existing stop_at_single_fail UI test pass.

Resolves #4729

[Copilot]

Pull request overview

Retains completed harness results when --fail-fast aborts verification, keeping summaries and JSON exports accurate.

Changes:

• Accumulates parallel results safely and restores harness ordering.
• Replaces schedule-dependent UI expectations with script-based checks.
• Adds a deterministic sequential regression test.

Reviewed changes

Copilot reviewed 10 out of 10 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
kani-driver/src/harness_runner.rs	Retains and sorts completed results.
tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.expected	Removes obsolete fixed summary.
tests/script-based-pre/fail_fast_parallel/fixture.rs	Updates parallel fixture documentation.
tests/script-based-pre/fail_fast_parallel/early_abort.sh	Checks parallel fail-fast behavior.
tests/script-based-pre/fail_fast_parallel/early_abort.expected	Adds expected script result.
tests/script-based-pre/fail_fast_parallel/config.yml	Configures parallel regression test.
tests/script-based-pre/fail_fast_keeps_completed/keeps_completed.sh	Checks deterministic result retention.
tests/script-based-pre/fail_fast_keeps_completed/keeps_completed.expected	Adds expected script result.
tests/script-based-pre/fail_fast_keeps_completed/fixture.rs	Adds passing and failing harnesses.
tests/script-based-pre/fail_fast_keeps_completed/config.yml	Configures sequential regression test.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.