Keep UI test programs free of integer overflow

[coord-e]

This is the next step toward dropping -C debug-assertions=off from the UI tests, after #291.

With debug assertions on, rustc checks for overflow on +, - and *. Since #280, Thrust verifies those checks. Many test programs use arithmetic that can really overflow, for example x + 1 with requires(true), or a counter in a loop with no bound. These tests fail with Unsat once the flag is gone.

This PR bounds the arithmetic in each of those tests by the integer type limits, using the associated consts from #296. It drops the flag from the 32 tests that then pass.

Changes

• Values from rand() are guarded by an if in the code that uses them, e.g. if i64::MIN <= a && a < i64::MAX && .... rand() itself keeps ensures(true).
• requires states that the operation fits the type, e.g. i64::MIN <= x + x && x + x <= i64::MAX. This applies to annot_forall, annot_preds, annot_raw_command*, annot_*formula_fn_mut, closure_* and closure_no_capture_fn_param.
• Loops stop at i64::MAX, or at HALF_MAX when they add two counters.
  • loop_invariant_nested also puts the bounds in its inner invariant, because an explicit invariant does not carry the outer guard's bound on x.
  • loop_invariant_trait_self resets the counter to 0 when it is out of range, in place of *= -1.
• annot_preds_trait*: Double gains a can_double predicate, and double requires it. A trait-level requires cannot name the implementor's fields.
• loop now uses PCSat. Z3 times out on it once the bound is added.

Integer values carry no range facts yet, which shapes the bounds in three ways:

• A bound is given on both sides even where the operation can only overflow in one direction. For example, annot_forall does not pass with only requires(x < i32::MAX).
• A guard in code compares only against constants. Arithmetic in the guard itself, such as i32::MAX - x, can overflow in the model.
• Thrust does not handle integer division in code, so i64::MAX / 2 is written as a const item (HALF_MAX, HALF_MIN).

Each fail file keeps the same bounds as its pass file. Where a fail file added arithmetic that the new bounds would let overflow, it now breaks the property without overflowing:

• annot_exists, annot_exists_formula_fn, annot_preds: x + x + 1 in place of x + x + x.
• annot_exists_formula_fn_mut: requires(x >= 0 && ...) in place of *m -= x.
• recursive: assert!(y != x) in place of y == x + 1.
• loop_invariant_nested: keeps the new bounds on x and still drops the clauses on y.

Tests

cargo test passes on all 384 UI tests, run locally with Z3 5.0.0 and the pinned PCSat binary.

Not covered

These tests still need -C debug-assertions=off:

• Solver does not finish once bounded:
  • Timeout: mut_recursive (Z3 and PCSat); closure_receiver_mut_model, closure_receiver_mut_model_byval; the fail side of option_map.
  • Unknown/Unsat: loop_invariant_fn_param_closure. This is not investigated.
• Need range facts: fn_poly_annot_2 (x * 1), fn_poly_annot_recursive, mod_invariant, iterators/annot_range_*, slice_split_first_loop*, loop_invariant_fn_param_at_entry.
• Thrust bugs:
  • slice_index_mut: checked compound assignment to a slice element panics in elaborate_place_for_borrow.
  • ghost_field, ghost_self: once overflow checks split the block, a ghost parameter is no longer live.
• Other: the fail side of iterators/fixed_filter_loop_none times out.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PzcoivHkYESNWJykaKpAmR

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-28T23:56:16.324869Z	571c4c7	New commits

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.