Identify annotation quantified variables by a system-unique ID

[coord-e]

Fixes #312.

A variable bound by forall/exists in an annotation was represented as Term::FormulaQuantifiedVar(Sort, String), tied to its quantifier by the source name alone. pre!(f(..))/post!(f(..), ..) build the closure's annotation formula with its parameters replaced by argument terms from the caller's annotation. When an argument contains the caller's quantified variable (such as the i in Option::map's spec exists(|i| opt == Some(i) && pre!(f(i)))) and the closure's formula has a quantifier with the same name, the two can't be told apart, and the inner quantifier binds both. Here is an example:

let half = thrust_macros::closure!(
    requires(exists(|i: i64| x == i + i)),
    |x: i64| -> i64 { assert!(x != 3); x },
);
let _ = Some(3).map(half);

This verified as safe, although the closure panics on 3.

Change

• Term::FormulaQuantifiedVar(Sort, String) → Term::UserQuantifiedVar(Sort, UserQuantifiedVarId). Formula::Exists/Forall bind Vec<(UserQuantifiedVarId, Sort)>.
• UserQuantifiedVarId is issued by System::new_user_quantified_var, so it is unique in the CHC system like PredVarId. The annotation translator gets one per quantified variable through Analyzer::generate_user_quantified_var.
• SMT-LIB and debug output print the ID as q$<n>. The q$ prefix keeps these names apart from the generated clause variables, as in Keep spec quantifier binders from capturing clause variables #295.

Testing

• With PCSat, the example above is rejected with Unsat, and Some(4).map(half) verifies. No test is added for it.
• cargo test, cargo fmt --check and cargo clippy -D warnings pass locally.

🤖 Generated with Claude Code

https://claude.ai/code/session_0188UiLozh1wCkmzZxJvzUTS

[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-30T22:36:46.542891Z	6d92151	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.

[coord-e]

test failed on 163b579 in tests/ui/fail/slice_split_first_mut_loop.rs: verification error: Timeout(60s) under PCSat, where Unsat is expected. The other 385 tests passed.

I don't think this PR causes it. The test has no forall/exists, and with comments stripped the SMT-LIB it emits is byte-identical on main and on this branch (776 lines). So the solver gets the same query either way. The same test passed on this PR's previous commit (54251fd) and in my local run. It has been unstable before: it was removed and restored in c8f600a, and its timeout was extended in bf7ddd3. No fix exists for the instability yet. I'm re-running the failed job once.

---

Generated by Claude Code