Fix exit code swallowed by --quiet on verification failure

kani-driver/src/harness_runner.rs

@@ -306,10 +306,6 @@ impl KaniSession {
     /// Note: Takes `self` "by ownership". This function wants to be able to drop before
     /// exiting with an error code, if needed.
     pub(crate) fn print_final_summary(self, results: &[HarnessResult<'_>]) -> Result<()> {
-        if self.args.common_args.quiet {
-            return Ok(());
-        }
-
         let (automatic, manual): (Vec<_>, Vec<_>) =
             results.iter().partition(|r| r.harness.is_automatically_generated);
 
@@ -320,6 +316,21 @@ impl KaniSession {
         let failing = failures.len();
         let total = succeeding + failing;
 
+        // Failure count of automatically generated harnesses, computed without printing so the
+        // `--quiet` path below stays honest. Must match `print_autoharness_summary`'s partition.
+        let autoharness_failing_count =
+            automatic.iter().filter(|r| r.result.status != VerificationStatus::Success).count();
+
+        if self.args.common_args.quiet {
+            // `--quiet` suppresses all output, but never the exit status: a failing
+            // verification must exit nonzero even when nothing is printed.
+            if failing + autoharness_failing_count > 0 {
+                drop(self);
+                std::process::exit(1);
+            }
+            return Ok(());
+        }
+
         if self.args.concrete_playback.is_some() {
             if failures.is_empty() {
                 println!(

tests/script-based-pre/quiet-exit-code/config.yml

@@ -0,0 +1,3 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: quiet-exit-code.sh

tests/script-based-pre/quiet-exit-code/failing.rs

@@ -0,0 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn failing_harness() {
+    assert!(1 == 2);
+}

tests/script-based-pre/quiet-exit-code/passing.rs

@@ -0,0 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn passing_harness() {
+    assert!(1 == 1);
+}

tests/script-based-pre/quiet-exit-code/quiet-exit-code.sh

@@ -0,0 +1,38 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Regression test for https://github.com/model-checking/kani/issues/4745:
+# `--quiet` must suppress output but never the exit status. A failing
+# verification under `--quiet` must exit nonzero; a passing one must exit 0;
+# both must produce no output.
+
+set -eu
+
+cd $(dirname $0)
+rm -f quiet-fail.out quiet-pass.out
+
+echo "Checking --quiet on a failing harness..."
+if kani --quiet failing.rs > quiet-fail.out 2>&1; then
+    echo "Error: kani --quiet on a failing harness exited 0 (failure masked as pass)."
+    exit 1
+fi
+if [ -s quiet-fail.out ]; then
+    echo "Error: kani --quiet produced output on the failing run:"
+    cat quiet-fail.out
+    exit 1
+fi
+
+echo "Checking --quiet on a passing harness..."
+if ! kani --quiet passing.rs > quiet-pass.out 2>&1; then
+    echo "Error: kani --quiet on a passing harness exited nonzero."
+    exit 1
+fi
+if [ -s quiet-pass.out ]; then
+    echo "Error: kani --quiet produced output on the passing run:"
+    cat quiet-pass.out
+    exit 1
+fi
+
+rm -f quiet-fail.out quiet-pass.out
+echo "Finished quiet exit-code check successfully."