Fix exit code swallowed by --quiet on verification failure - #4787
Open
rbeauchamp wants to merge 1 commit into
Open
Fix exit code swallowed by --quiet on verification failure#4787rbeauchamp wants to merge 1 commit into
rbeauchamp wants to merge 1 commit into
Conversation
This was referenced Sep 8, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
kani --quiet(andcargo kani --quiet) always exits 0, even when verification fails.print_final_summaryinkani-driver/src/harness_runner.rsreturnedOk(())early under--quiet, skipping theprocess::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 --quieton 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/: runskani --quieton 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-driverpasses (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.