Show variable origins and clause context in SMT2 comments

[coord-e]

SMT2 variables such as v0 do not show which environment binding or refinement variable they represent. Preserve this information in dedicated clause-origin types and print it before each assert, with the environment under Γ, assumptions as _: { p }, and grouped body entries followed by head. Variable mappings appear directly beneath the corresponding entry, including existential variables, without changing SMT variable names.

A separate commit fixes an extra leading space when pretty-printing atoms without guards.

Validation: cargo test --lib (3 passed), cargo fmt --all -- --check, the passing and failing simple_mut examples with Z3, and annot_exists with PCSat. The layout change preserves the non-comment SMT tokens in the simple_mut output.

[Copilot]

Copilot review overview

🟢 Approval recommended

Only a minor request for regression coverage remains; no approval-blocking issues were identified.

Review effort: Balanced
Findings: None

What changed in this PR

Adds source-level provenance to SMT-LIB2 comments while preserving solver-facing constraints and variable names.

Changes:

• Tracks environment, body, head, and existential origins.
• Prints structured origin comments before assertions.
• Fixes leading whitespace for unguarded atoms.

File	Description
src/​rty/​subtyping.rs	Records function parameter origins.
src/​rty/​clause_builder.rs	Records refinement and existential mappings.
src/​refine/​env.rs	Captures binding and assumption origins.
src/​chc/​unbox.rs	Preserves origins during unboxing.
src/​chc/​smtlib2.rs	Renders structured clause-origin comments.
src/​chc/​debug/​origin.rs	Defines provenance metadata and mappings.
src/​chc/​debug.rs	Exposes the origin module.
src/​chc/​clause_builder.rs	Propagates origins into generated clauses.
src/​chc.rs	Adds origins and fixes atom formatting.
src/​analyze/​crate_.rs	Records entry-parameter mappings.
src/​analyze/​basic_block.rs	Records block parameter and assumption origins.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.
To continue using code reviews, you can upgrade your account or add credits to your account and enable them for code reviews in your settings.