Fail verification when the solver backend drops quantifiers

[tautschnig]

Description

CBMC's SAT-based backends only support quantifiers with constant bounds (boolbv_quantifier.cpp's eager instantiation). A kani::forall!/kani::exists! with a symbolic bound reaches the backend's quantifier post-processing, which has no handling: the expression is replaced with unconstrained values, and CBMC reports only a low-visibility warning: ignoring forall among its status messages — which Kani currently swallows entirely.

The consequences are severe for usability:

• a kani::assume containing such a quantifier is silently not enforced: the harness may report VERIFICATION:- SUCCESSFUL while covering none of the intended property (found while building quantified element-validity assumptions for autoharness slice generation, where the vacuous assume was only caught by a non-tautological probe);
• a kani::assert containing one may fail spuriously.

This PR detects CBMC's ignoring-quantifier messages in the output parser, counts them on VerificationResult, and renders a prominent warning after the result (on both successful and failed outcomes), explaining the effect and suggesting #[kani::solver(z3)], which handles these quantifiers (verified: the same harnesses verify correctly, fast, under z3).

A proper fix (quantifier instantiation in CBMC's SAT backend) is in progress upstream; this warning closes the silent-degradation window until it lands.

Testing

New expected test pins the dangerous case: a harness that succeeds only because its assertion does not depend on the (unenforced) quantified assumption, with the warning attached. Verified no-warning behavior for constant-bound quantifiers (eagerly instantiated) and under --solver z3. All quantifier expected tests and kani-driver unit tests pass.

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

[Copilot]

Pull request overview

This PR improves Kani’s user-facing diagnostics around CBMC SAT-backend quantifiers by detecting CBMC “ignoring forall/exists” messages, tracking how many quantifier expressions were dropped, and emitting a prominent warning so users don’t mistake vacuous assumes (or spurious assert failures) for reliable results.

Changes:

• Add parsing/counting of CBMC “ignoring forall/exists” messages and plumb the count into VerificationResult.
• Render a prominent, multi-line warning when dropped quantifiers are detected.
• Add a new expected test that pins the dangerous “vacuous assume” scenario and asserts the warning is emitted.

Reviewed changes

Copilot reviewed 4 out of 5 changed files in this pull request and generated 1 comment.

File	Description
tests/expected/quantifiers/ignored_quantifier_warning.rs	New regression test harness that triggers a symbolic-bound quantifier being dropped.
tests/expected/quantifiers/ignored_quantifier_warning.expected	Expected output asserting the new prominent warning is printed.
kani-driver/src/call_cbmc.rs	Counts ignored-quantifier messages and renders a warning via VerificationResult.
Cargo.lock	Updates locked charon version (appears unrelated to the PR’s stated scope).

Suppressed comments (1)

kani-driver/src/call_cbmc.rs:461

• The ignored-quantifier warning is appended after format_result/format_coverage, which already ends with the final VERIFICATION:- ... line. This means the warning currently prints after the overall status line (and with an extra blank line), but the new expected test output places the warning before VERIFICATION:- ... so it’s not missed on successful runs.

                if self.ignored_quantifiers > 0 {
                    result.push('\n');
                    result.push_str(&ignored_quantifiers_warning(self.ignored_quantifiers));
                }

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[feliperodri]

Behavior change (experimental -Z quantifiers): Previously, when the SAT solver backend dropped a quantifier with non-constant bounds, Kani printed a warning but still reported SUCCESSFUL. Because a kani::assume containing such a quantifier is silently not enforced, that "success" could be vacuous (an unsound false negative). Kani now reports VERIFICATION:- FAILED in this case and directs users to an SMT backend that supports quantifiers (e.g., #[kani::solver(z3)]). Proofs that relied on the old warn-and-pass behavior will now fail — correctly.

@tautschnig do you agree to merge it with this new behavior?