From 65c183c6906468c1fff027bbfe2fc5d4b2cc263f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 5 Aug 2026 21:22:09 +0000 Subject: [PATCH 1/4] Warn prominently when the solver backend drops quantifiers CBMC's SAT-based backends only support quantifiers with constant bounds. A quantifier with a symbolic bound reaches the backend's quantifier post-processing, which has no handling and replaces the expression with unconstrained values, reporting only a low-visibility 'warning: ignoring forall' among CBMC's status messages (which Kani does not surface). The consequences are severe for usability: a kani::assume containing such a quantifier is silently NOT enforced -- the harness may verify successfully while covering none of the intended property -- and a kani::assert containing one may fail spuriously. Detect CBMC's ignoring-quantifier messages in the output parser, count them on VerificationResult, and render a prominent warning after the result (on both successful and failed outcomes) explaining the effect and suggesting an SMT solver backend (#[kani::solver(z3)]), which supports these quantifiers. The new expected test pins the dangerous case: a harness that SUCCEEDS only because its final assertion does not depend on the (unenforced) quantified assumption, with the warning attached. Co-authored-by: Kiro --- Cargo.lock | 2 +- charon | 2 +- kani-driver/src/call_cbmc.rs | 47 ++++++++++++++++++- .../ignored_quantifier_warning.expected | 4 ++ .../quantifiers/ignored_quantifier_warning.rs | 26 ++++++++++ 5 files changed, 78 insertions(+), 3 deletions(-) create mode 100644 tests/expected/quantifiers/ignored_quantifier_warning.expected create mode 100644 tests/expected/quantifiers/ignored_quantifier_warning.rs diff --git a/Cargo.lock b/Cargo.lock index 0ba3f8aaab8..482bf84cbf8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -288,7 +288,7 @@ checksum = "f079e83a288787bcd14a6aea84cee5c87a67c5a3e660c30f557a3d24761b3527" [[package]] name = "charon" -version = "0.1.88" +version = "0.1.73" dependencies = [ "annotate-snippets", "anstream 0.6.21", diff --git a/charon b/charon index 607f5683aee..dee6603064c 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit 607f5683aee39a427267f8cdc1aa15735b096a1a +Subproject commit dee6603064c23aa331efc58802e7b511eb405f35 diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 6891d49fd66..beef87e9be9 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -18,7 +18,7 @@ use tokio::process::Command as TokioCommand; use crate::args::common::Verbosity; use crate::args::{OutputFormat, VerificationArgs}; use crate::cbmc_output_parser::{ - CheckStatus, Property, VerificationOutput, extract_results, process_cbmc_output, + CheckStatus, ParserItem, Property, VerificationOutput, extract_results, process_cbmc_output, }; use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter}; use crate::coverage::cov_results::{CoverageCheck, CoverageResults}; @@ -75,6 +75,12 @@ pub struct VerificationResult { pub runtime: Duration, /// Whether concrete playback generated a test pub generated_concrete_test: bool, + /// The number of quantifier expressions CBMC's solver backend could not encode and + /// dropped (replaced with unconstrained values), c.f. CBMC's "warning: ignoring forall" + /// messages. Nonzero counts make results unreliable: an `assume` containing such a + /// quantifier is not enforced (a successful result may be vacuous), and an `assert` + /// containing one may fail spuriously. + pub ignored_quantifiers: usize, /// The coverage results pub coverage_results: Option, } @@ -162,6 +168,7 @@ impl KaniSession { results: Err(ExitStatus::Timeout), runtime: start_time.elapsed(), generated_concrete_test: false, + ignored_quantifiers: 0, coverage_results: None, }) } @@ -323,6 +330,35 @@ impl KaniSession { } } +/// Count CBMC messages reporting that a quantifier expression could not be encoded and was +/// dropped. CBMC's SAT-based backends only support quantifiers with constant bounds; other +/// quantifiers are replaced by unconstrained values, with only a low-visibility message +/// (`prop_conv_solvert::ignoring`, printed as "warning: ignoring forall" followed by the +/// pretty-printed expression). +fn count_ignored_quantifiers(items: &[ParserItem]) -> usize { + items + .iter() + .filter(|item| { + matches!(item, ParserItem::Message { message_text, .. } + if message_text.starts_with("warning: ignoring forall") + || message_text.starts_with("warning: ignoring exists")) + }) + .count() +} + +/// The warning rendered when the solver backend dropped quantifier expressions. +fn ignored_quantifiers_warning(count: usize) -> String { + format!( + "warning: the solver backend does not support quantifiers with non-constant bounds \ +and ignored {count} quantifier expression(s), replacing them with unconstrained values.\n\ + Verification results are unreliable: `kani::assume` calls containing such a \ +quantifier are NOT enforced (a successful result may not cover the intended property), and \ +`kani::assert` calls containing one may fail spuriously.\n\ + Consider using an SMT solver backend, e.g. `#[kani::solver(z3)]`, which supports \ +these quantifiers.\n" + ) +} + impl VerificationResult { /// Computes a `VerificationResult` (kani-driver's notion of the result of a CBMC call) from a /// `VerificationOutput` (cbmc_output_parser's idea of CBMC results). @@ -338,6 +374,7 @@ impl VerificationResult { start_time: Instant, ) -> VerificationResult { let runtime = start_time.elapsed(); + let ignored_quantifiers = count_ignored_quantifiers(&output.processed_items); let (_, results) = extract_results(output.processed_items); if let Some(results) = results { @@ -350,6 +387,7 @@ impl VerificationResult { results: Ok(results), runtime, generated_concrete_test: false, + ignored_quantifiers, coverage_results, } } else { @@ -365,6 +403,7 @@ impl VerificationResult { results: Err(exit_status), runtime, generated_concrete_test: false, + ignored_quantifiers, coverage_results: None, } } @@ -377,6 +416,7 @@ impl VerificationResult { results: Ok(vec![]), runtime: Duration::from_secs(0), generated_concrete_test: false, + ignored_quantifiers: 0, coverage_results: None, } } @@ -391,6 +431,7 @@ impl VerificationResult { results: Err(ExitStatus::Other(42)), runtime: Duration::from_secs(0), generated_concrete_test: false, + ignored_quantifiers: 0, coverage_results: None, } } @@ -414,6 +455,10 @@ impl VerificationResult { } else { format_result(results, status, should_panic, failed_properties, show_checks) }; + if self.ignored_quantifiers > 0 { + result.push('\n'); + result.push_str(&ignored_quantifiers_warning(self.ignored_quantifiers)); + } writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap(); result } diff --git a/tests/expected/quantifiers/ignored_quantifier_warning.expected b/tests/expected/quantifiers/ignored_quantifier_warning.expected new file mode 100644 index 00000000000..38de5ea982e --- /dev/null +++ b/tests/expected/quantifiers/ignored_quantifier_warning.expected @@ -0,0 +1,4 @@ +warning: the solver backend does not support quantifiers with non-constant bounds and ignored 1 quantifier expression(s), replacing them with unconstrained values. +Verification results are unreliable: `kani::assume` calls containing such a quantifier are NOT enforced (a successful result may not cover the intended property), and `kani::assert` calls containing one may fail spuriously. +Consider using an SMT solver backend, e.g. `#[kani::solver(z3)]`, which supports these quantifiers. +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/quantifiers/ignored_quantifier_warning.rs b/tests/expected/quantifiers/ignored_quantifier_warning.rs new file mode 100644 index 00000000000..71622d97289 --- /dev/null +++ b/tests/expected/quantifiers/ignored_quantifier_warning.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zquantifiers + +//! Test that Kani prominently warns when the solver backend drops a quantifier +//! it cannot encode. CBMC's SAT-based backends only support quantifiers with +//! constant bounds; a quantifier with a symbolic bound is replaced by an +//! unconstrained value (CBMC prints only a low-visibility "warning: ignoring +//! forall"). This silently vacuates `kani::assume`s: this harness SUCCEEDS, +//! but only because the final assertion does not depend on the (unenforced) +//! assumption -- which is exactly why the warning must be prominent. + +extern crate kani; + +#[kani::proof] +fn vacuous_assume_warns() { + let len: usize = kani::any(); + kani::assume(len >= 1 && len <= 100); + let layout = std::alloc::Layout::array::(len).unwrap(); + let p = unsafe { std::alloc::alloc(layout) }; + kani::assume(!p.is_null()); + unsafe { + kani::assume(kani::forall!(|i in (0, len)| *p.wrapping_add(i) < 60)); + } + assert!(len <= 100); +} From 7974f7ca1e5fc4dab15c934fdc0738f80525466d Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Fri, 14 Aug 2026 01:04:54 +0000 Subject: [PATCH 2/4] Fix quantifier-warning test wiring and surface the warning before the verdict Three fixes to the ignored-quantifier warning change: - Add the new `ignored_quantifiers` field to the two `VerificationResult` literals in `sarif.rs`'s test module. Without them `cargo test`/ `cargo clippy --tests` fail to compile (`missing field ignored_quantifiers`), which is what broke the clippy-check and the kani-driver unit tests in the regression job. - Rename the regression test from `ignored_quantifier_warning` to `dropped_quantifier_warning`. compiletest skips any test whose path contains "ignore" (see `tools/compiletest/src/header.rs`), so the test was silently ignored and never actually ran. - Render the warning immediately before the `VERIFICATION:- ...` line rather than after it, so a reliability warning is not missed when the run otherwise reports success (this also matches the order in the `.expected` file). Falls back to appending when there is no such line (e.g. coverage output). Signed-off-by: Felipe Monteiro --- kani-driver/src/call_cbmc.rs | 14 ++++++++++++-- kani-driver/src/sarif.rs | 2 ++ ...xpected => dropped_quantifier_warning.expected} | 0 ...er_warning.rs => dropped_quantifier_warning.rs} | 0 4 files changed, 14 insertions(+), 2 deletions(-) rename tests/expected/quantifiers/{ignored_quantifier_warning.expected => dropped_quantifier_warning.expected} (100%) rename tests/expected/quantifiers/{ignored_quantifier_warning.rs => dropped_quantifier_warning.rs} (100%) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index beef87e9be9..633785807c9 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -456,8 +456,18 @@ impl VerificationResult { format_result(results, status, should_panic, failed_properties, show_checks) }; if self.ignored_quantifiers > 0 { - result.push('\n'); - result.push_str(&ignored_quantifiers_warning(self.ignored_quantifiers)); + let warning = ignored_quantifiers_warning(self.ignored_quantifiers); + // Surface the reliability warning immediately before the overall + // `VERIFICATION:- ...` line, so it is not missed when the run otherwise + // reports success. Fall back to appending it (e.g. coverage output, which + // has no such line) if the marker isn't present. + match result.find("\nVERIFICATION:- ") { + Some(pos) => result.insert_str(pos + 1, &warning), + None => { + result.push('\n'); + result.push_str(&warning); + } + } } writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap(); result diff --git a/kani-driver/src/sarif.rs b/kani-driver/src/sarif.rs index 849c48c7c2d..877f39b0fa0 100644 --- a/kani-driver/src/sarif.rs +++ b/kani-driver/src/sarif.rs @@ -326,6 +326,7 @@ mod tests { results: Err(ExitStatus::Timeout), runtime: Duration::from_secs(1), generated_concrete_test: false, + ignored_quantifiers: 0, coverage_results: None, } } @@ -339,6 +340,7 @@ mod tests { results: Ok(vec![failure_property()]), runtime: Duration::from_secs(1), generated_concrete_test: false, + ignored_quantifiers: 0, coverage_results: None, }; let harness_result = HarnessResult { harness: &harness, result }; diff --git a/tests/expected/quantifiers/ignored_quantifier_warning.expected b/tests/expected/quantifiers/dropped_quantifier_warning.expected similarity index 100% rename from tests/expected/quantifiers/ignored_quantifier_warning.expected rename to tests/expected/quantifiers/dropped_quantifier_warning.expected diff --git a/tests/expected/quantifiers/ignored_quantifier_warning.rs b/tests/expected/quantifiers/dropped_quantifier_warning.rs similarity index 100% rename from tests/expected/quantifiers/ignored_quantifier_warning.rs rename to tests/expected/quantifiers/dropped_quantifier_warning.rs From 26a078945d92f5e98a15dc94e7deb5410284a3ff Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Fri, 14 Aug 2026 16:21:35 +0000 Subject: [PATCH 3/4] Revert accidental charon submodule downgrade Commit 65c183c ("Warn prominently when the solver backend drops quantifiers") inadvertently swept in a stale charon submodule pointer (607f5683 -> dee66030, a downgrade from 0.1.88 to 0.1.73) and the matching Cargo.lock change. These are unrelated to the quantifier warning feature. Restore charon to 607f5683 / 0.1.88. --- Cargo.lock | 2 +- charon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 482bf84cbf8..0ba3f8aaab8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -288,7 +288,7 @@ checksum = "f079e83a288787bcd14a6aea84cee5c87a67c5a3e660c30f557a3d24761b3527" [[package]] name = "charon" -version = "0.1.73" +version = "0.1.88" dependencies = [ "annotate-snippets", "anstream 0.6.21", diff --git a/charon b/charon index dee6603064c..607f5683aee 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit dee6603064c23aa331efc58802e7b511eb405f35 +Subproject commit 607f5683aee39a427267f8cdc1aa15735b096a1a From 32af783b15617a996685b813c30dbe863f26b7e9 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Fri, 14 Aug 2026 20:49:59 +0000 Subject: [PATCH 4/4] Escalate dropped-quantifier warning to a verification failure When CBMC's SAT backend cannot encode a quantifier with non-constant bounds, it drops it and replaces it with an unconstrained value. A `kani::assume` containing such a quantifier is then silently not enforced, so a "SUCCESSFUL" verdict can be vacuous -- an unsound false negative, which Kani must never produce. Instead of only printing a warning, force the verification to FAIL (VerificationStatus::Failure / FailedProperties::Error) when any quantifier was dropped, and render an error directing users to an SMT solver backend that supports quantifiers, e.g. `#[kani::solver(z3)]`. Also: - Fix a merge-integration bug: schema_utils_test.rs constructed VerificationResult without the `ignored_quantifiers` field, breaking the test build. - Rename the dropped_quantifier_warning expected test to dropped_quantifier_error and update it to assert VERIFICATION:- FAILED. - Document the solver-backend limitation in the quantifiers reference. --- .../src/reference/experimental/quantifiers.md | 6 +++ kani-driver/src/call_cbmc.rs | 44 +++++++++++-------- .../src/frontend/tests/schema_utils_test.rs | 2 + .../dropped_quantifier_error.expected | 4 ++ .../quantifiers/dropped_quantifier_error.rs | 27 ++++++++++++ .../dropped_quantifier_warning.expected | 4 -- .../quantifiers/dropped_quantifier_warning.rs | 26 ----------- 7 files changed, 65 insertions(+), 48 deletions(-) create mode 100644 tests/expected/quantifiers/dropped_quantifier_error.expected create mode 100644 tests/expected/quantifiers/dropped_quantifier_error.rs delete mode 100644 tests/expected/quantifiers/dropped_quantifier_warning.expected delete mode 100644 tests/expected/quantifiers/dropped_quantifier_warning.rs diff --git a/docs/src/reference/experimental/quantifiers.md b/docs/src/reference/experimental/quantifiers.md index a38698a8023..b86501911d4 100644 --- a/docs/src/reference/experimental/quantifiers.md +++ b/docs/src/reference/experimental/quantifiers.md @@ -54,3 +54,9 @@ fn vec_assert_forall_harness() { We now assume that all quantified variables are of type `usize`. This means that the range specified in the quantifier must be compatible with `usize`. We plan to support other types in the future, but for now, ensure that your quantifiers use `usize` ranges. + +#### Solver Backend Support + +The default SAT-based solver backend only supports quantifiers with constant bounds. A quantifier whose bound is symbolic (not known at compile time) cannot be encoded and would be silently replaced with an unconstrained value, which is unsound: a `kani::assume` containing such a quantifier would not be enforced, and a `kani::assert` containing one could fail spuriously. + +To keep results sound, Kani reports verification as `FAILED` when the backend drops a quantifier, and directs you to an SMT solver backend that supports quantifiers. Use `#[kani::solver(z3)]` on the harness (or `--solver z3` on the command line) to verify these quantifiers. diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index cd33ea29652..9a9ef2b4009 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -212,9 +212,10 @@ pub struct VerificationResult { pub generated_concrete_test: bool, /// The number of quantifier expressions CBMC's solver backend could not encode and /// dropped (replaced with unconstrained values), c.f. CBMC's "warning: ignoring forall" - /// messages. Nonzero counts make results unreliable: an `assume` containing such a - /// quantifier is not enforced (a successful result may be vacuous), and an `assert` - /// containing one may fail spuriously. + /// messages. A nonzero count makes the analysis unsound -- an `assume` containing such a + /// quantifier is not enforced (a successful result would be vacuous), and an `assert` + /// containing one may fail spuriously -- so it forces the verification to fail (see + /// `VerificationResult::from`). pub ignored_quantifiers: usize, /// The coverage results pub coverage_results: Option, @@ -492,16 +493,15 @@ fn count_ignored_quantifiers(items: &[ParserItem]) -> usize { .count() } -/// The warning rendered when the solver backend dropped quantifier expressions. -fn ignored_quantifiers_warning(count: usize) -> String { +/// The error rendered when the solver backend dropped quantifier expressions. +fn ignored_quantifiers_error(count: usize) -> String { format!( - "warning: the solver backend does not support quantifiers with non-constant bounds \ + "error: the solver backend does not support quantifiers with non-constant bounds \ and ignored {count} quantifier expression(s), replacing them with unconstrained values.\n\ - Verification results are unreliable: `kani::assume` calls containing such a \ -quantifier are NOT enforced (a successful result may not cover the intended property), and \ + Kani cannot soundly verify this harness: `kani::assume` calls containing such a \ +quantifier are NOT enforced (a successful result would not cover the intended property), and \ `kani::assert` calls containing one may fail spuriously.\n\ - Consider using an SMT solver backend, e.g. `#[kani::solver(z3)]`, which supports \ -these quantifiers.\n" + Use an SMT solver backend that supports quantifiers, e.g. `#[kani::solver(z3)]`.\n" ) } @@ -529,8 +529,16 @@ impl VerificationResult { let cbmc_stats = if collect_cbmc_stats { merge_cbmc_stats(&remaining_items) } else { None }; if let Some(results) = results { - let (status, failed_properties) = + let (mut status, mut failed_properties) = verification_outcome_from_properties(&results, should_panic); + // A dropped quantifier makes the analysis unsound: a `kani::assume` containing one is + // silently not enforced, so a "successful" result may be vacuous. Kani must never + // report success in that case -- force a failure and (via the rendered error) direct + // the user to an SMT backend that supports quantifiers. + if ignored_quantifiers > 0 { + status = VerificationStatus::Failure; + failed_properties = FailedProperties::Error; + } let coverage_results = coverage_results_from_properties(&results); VerificationResult { status, @@ -611,16 +619,16 @@ impl VerificationResult { format_result(results, status, should_panic, failed_properties, show_checks) }; if self.ignored_quantifiers > 0 { - let warning = ignored_quantifiers_warning(self.ignored_quantifiers); - // Surface the reliability warning immediately before the overall - // `VERIFICATION:- ...` line, so it is not missed when the run otherwise - // reports success. Fall back to appending it (e.g. coverage output, which - // has no such line) if the marker isn't present. + let error = ignored_quantifiers_error(self.ignored_quantifiers); + // Surface the soundness error immediately before the overall + // `VERIFICATION:- ...` line, so it explains the forced failure. Fall back to + // appending it (e.g. coverage output, which has no such line) if the marker + // isn't present. match result.find("\nVERIFICATION:- ") { - Some(pos) => result.insert_str(pos + 1, &warning), + Some(pos) => result.insert_str(pos + 1, &error), None => { result.push('\n'); - result.push_str(&warning); + result.push_str(&error); } } } diff --git a/kani-driver/src/frontend/tests/schema_utils_test.rs b/kani-driver/src/frontend/tests/schema_utils_test.rs index f1693cad5a1..d7887c8c4f4 100644 --- a/kani-driver/src/frontend/tests/schema_utils_test.rs +++ b/kani-driver/src/frontend/tests/schema_utils_test.rs @@ -134,6 +134,7 @@ fn test_create_verification_result_json() { results: Ok(properties), runtime: Duration::from_millis(120), generated_concrete_test: false, + ignored_quantifiers: 0, coverage_results: None, cbmc_stats: None, }; @@ -207,6 +208,7 @@ fn test_add_runner_results_to_json_real() { results: Err(ExitStatus::Other(42)), runtime: Duration::from_millis(120), generated_concrete_test: false, + ignored_quantifiers: 0, coverage_results: None, cbmc_stats: None, }; diff --git a/tests/expected/quantifiers/dropped_quantifier_error.expected b/tests/expected/quantifiers/dropped_quantifier_error.expected new file mode 100644 index 00000000000..421827b0627 --- /dev/null +++ b/tests/expected/quantifiers/dropped_quantifier_error.expected @@ -0,0 +1,4 @@ +error: the solver backend does not support quantifiers with non-constant bounds and ignored 1 quantifier expression(s), replacing them with unconstrained values. +Kani cannot soundly verify this harness: `kani::assume` calls containing such a quantifier are NOT enforced (a successful result would not cover the intended property), and `kani::assert` calls containing one may fail spuriously. +Use an SMT solver backend that supports quantifiers, e.g. `#[kani::solver(z3)]`. +VERIFICATION:- FAILED diff --git a/tests/expected/quantifiers/dropped_quantifier_error.rs b/tests/expected/quantifiers/dropped_quantifier_error.rs new file mode 100644 index 00000000000..2a701fc23d7 --- /dev/null +++ b/tests/expected/quantifiers/dropped_quantifier_error.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zquantifiers + +//! Test that Kani fails with a sound-analysis error when the solver backend +//! drops a quantifier it cannot encode. CBMC's SAT-based backends only support +//! quantifiers with constant bounds; a quantifier with a symbolic bound is +//! replaced by an unconstrained value (CBMC prints only a low-visibility +//! "warning: ignoring forall"). That silently vacuates `kani::assume`s: without +//! intervention this harness would report SUCCESSFUL only because the final +//! assertion does not depend on the (unenforced) assumption -- an unsound false +//! negative. Kani must instead surface the error and force a failure. + +extern crate kani; + +#[kani::proof] +fn vacuous_assume_warns() { + let len: usize = kani::any(); + kani::assume(len >= 1 && len <= 100); + let layout = std::alloc::Layout::array::(len).unwrap(); + let p = unsafe { std::alloc::alloc(layout) }; + kani::assume(!p.is_null()); + unsafe { + kani::assume(kani::forall!(|i in (0, len)| *p.wrapping_add(i) < 60)); + } + assert!(len <= 100); +} diff --git a/tests/expected/quantifiers/dropped_quantifier_warning.expected b/tests/expected/quantifiers/dropped_quantifier_warning.expected deleted file mode 100644 index 38de5ea982e..00000000000 --- a/tests/expected/quantifiers/dropped_quantifier_warning.expected +++ /dev/null @@ -1,4 +0,0 @@ -warning: the solver backend does not support quantifiers with non-constant bounds and ignored 1 quantifier expression(s), replacing them with unconstrained values. -Verification results are unreliable: `kani::assume` calls containing such a quantifier are NOT enforced (a successful result may not cover the intended property), and `kani::assert` calls containing one may fail spuriously. -Consider using an SMT solver backend, e.g. `#[kani::solver(z3)]`, which supports these quantifiers. -VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/quantifiers/dropped_quantifier_warning.rs b/tests/expected/quantifiers/dropped_quantifier_warning.rs deleted file mode 100644 index 71622d97289..00000000000 --- a/tests/expected/quantifiers/dropped_quantifier_warning.rs +++ /dev/null @@ -1,26 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zquantifiers - -//! Test that Kani prominently warns when the solver backend drops a quantifier -//! it cannot encode. CBMC's SAT-based backends only support quantifiers with -//! constant bounds; a quantifier with a symbolic bound is replaced by an -//! unconstrained value (CBMC prints only a low-visibility "warning: ignoring -//! forall"). This silently vacuates `kani::assume`s: this harness SUCCEEDS, -//! but only because the final assertion does not depend on the (unenforced) -//! assumption -- which is exactly why the warning must be prominent. - -extern crate kani; - -#[kani::proof] -fn vacuous_assume_warns() { - let len: usize = kani::any(); - kani::assume(len >= 1 && len <= 100); - let layout = std::alloc::Layout::array::(len).unwrap(); - let p = unsafe { std::alloc::alloc(layout) }; - kani::assume(!p.is_null()); - unsafe { - kani::assume(kani::forall!(|i in (0, len)| *p.wrapping_add(i) < 60)); - } - assert!(len <= 100); -}