Warn when quantifier range exceeds SAT solver threshold

[feliperodri]

Emit a compile-time warning when an unbounded forall! or exists! quantifier is detected. SAT solvers (the default backend) expand quantifiers into one conjunction/disjunction per value in the range, so unbounded ranges (forall!(|i| ...) which expands over all 2^64 usize values) cause silent memory exhaustion or divergence with no diagnostic.

Contributes to #3273.

Problem

Writing forall!(|i| ...) (unbounded, ranging over all usize values) with the default SAT backend silently hangs or OOMs because CBMC expands the quantifier into 2^64 terms. Users get no feedback about why verification doesn't terminate.

Solution

• warn_large_quantifier_range() in hooks.rs: At codegen time, checks if both quantifier bounds are compile-time integer constants. If the range exceeds QUANTIFIER_RANGE_WARN_THRESHOLD (1000), emits a span_warn suggesting tighter bounds or an SMT solver. For unbounded ranges (~2^64), uses a human-friendly message instead of the raw integer.
• unwrap_to_constant(): Helper that unwraps typecasts and resolves symbol references via the symbol table to extract integer constants from bound expressions. Includes a depth limit (5) to guard against cycles.

Known limitation

Bounded quantifiers (forall!(|i in (0, 2000)| ...)) use let bindings in the macro expansion for type coercion, which hides the constant values from codegen. The warning currently only fires for unbounded quantifiers, which is the most dangerous case. Detecting large bounded ranges would require constant propagation through local variables, a potential follow-up improvement.

Example warning

warning: `kani::forall` has an unbounded (~2^64) range; SAT solvers (the default
         backend) expand quantifiers over every value and may exhaust memory or
         diverge. Consider adding tighter bounds or using an SMT solver
         (`#[kani::solver(z3)]` or `--solver z3`).
  --> tests/expected/quantifiers/large_range_warning.rs:15:13

Testing

• large_range_warning.rs — expected test with 3 harnesses:
  • check_unbounded_forall_warns: unbounded forall!(|i| ...), verifies warning is emitted
  • check_unbounded_exists_warns: unbounded exists!(|i| ...), verifies warning is emitted
  • check_small_forall_no_warn: range of 10, verifies no warning (absence of output is intentional)

---

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