Declare the sorts of quantifier binders in the emitted SMT-LIB2

[coord-e]

Closes #142.

collect_sorts gathers the sorts to declare from predicate signatures, clause variables and atom arguments. iter_atoms descends into the body of an Exists/Forall, but the binder list is metadata no atom references, so a sort that appears only as a binder is never collected and the query names an undefined sort — rejected while parsing, by any backend.

Fixing that alone turns the reported program into an ICE rather than a fix: enum definitions are collected from the local declarations of the body under analysis (basic_block::Analyzer::register_enum_defs), so an enum a specification only mentions as the type of a quantified variable is not in system.datatypes at all, and monomorphize_datatype unwraps a None on the now-collected sort. Both halves are needed.

Reading order

The diff is 4 source files, but only ~40 lines carry behavior; the commits are meant to be read one by one.

commit	what to check
7272014 Lift the enum definition collection out of the basic block analyzer	Pure move — EnumCollector is unchanged, it takes the TypeBuilder by reference instead of cloning it and walks one type per call instead of a loop of locals. The one behavioral nuance: visited no longer spans the whole local list, which only means a type shared by two locals is walked twice; get_or_register_enum_def is idempotent.
4f232a3 Register the enums a quantified variable's type is built from	Two lines in AnnotFnTranslator::to_formula_with_quantified_vars. No effect on its own — nothing yet asks for the binder's sort.
9ef66ff Declare the sorts of quantifier binders in the emitted SMT-LIB2	The actual fix plus the tests: iter_quantified_vars on Formula/Atom/Body in chc.rs, mirroring the shape of iter_atoms/fv next to them, and five lines in collect_sorts.

Atom::iter_quantified_vars covers the guard because smtlib2::Atom renders it as (=> guard ...), so a quantifier there needs its sorts declared too, exactly like one in the body formula. The issue also suggests inserting the sort in the FormulaQuantifiedVar arm of term_sorts; that arm is already covered by the sorts.insert(clause.term_sort(t)) at the top of the function, so it is left alone.

Testing

Verified against Z3 5.0.0 and the COAR image CI pins. cargo test passes (332 UI tests, plus doc tests); cargo fmt --check and cargo clippy -- -D warnings are clean.

The program from the issue, which reported unknown sort 'E' before:

$ THRUST_OUTPUT_DIR=/tmp/out cargo run -q -- -Adead_code -C debug-assertions=false repro.rs
$ grep -c declare-datatype /tmp/out/thrust_output.smt2
1

Under Z3 the query is now well-formed but comes back unknown, as any quantified specification does; under PCSat it verifies.

Tests added

Two pass/fail pairs, both quantifying over a sort that appears nowhere else in the clause, which is what it takes to reach the bug — a binder used in the body has its sort collected through the atom arguments already:

• tests/ui/{pass,fail}/annot_exists_enum_binder.rs — an enum-sorted binder, the case in the issue
• tests/ui/{pass,fail}/annot_exists_tuple_binder.rs — a tuple-sorted binder, the second reproduction in the issue

One caveat worth knowing before reviewing them: PCSat, which the quantifier tests have to use, accepts the malformed query instead of rejecting it, so the pass files verify even without this change — under Z3 they fail loudly. What they do pin under CI is the ICE: with the sort collected and the registration reverted, pass/annot_exists_enum_binder.rs panics. I could not find a program that pins the declaration itself through PCSat; if you would rather have that covered, a unit test over FormatContext::from_system with a hand-built system would do it, and I am happy to add one.

---

Generated by Claude Code

[Copilot]

🟡 Changes recommended

The added UI tests do not detect regression of the central SMT declaration fix because their solver accepts malformed input.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

Fixes missing SMT datatype declarations for sorts used only by quantifier binders.

Changes:

• Collects quantified-variable sorts from clauses, bodies, and atom guards.
• Registers enum definitions reachable from quantified parameter types.
• Adds enum and tuple binder UI test pairs.

File summaries

File	Description
src/chc/format_context.rs	Collects binder sorts for SMT formatting.
src/chc.rs	Adds recursive quantified-variable iterators.
src/analyze.rs	Centralizes enum-definition collection.
src/analyze/basic_block.rs	Uses the centralized enum collector.
src/analyze/annot_fn.rs	Registers enums used by quantified parameters.
tests/ui/pass/annot_exists_enum_binder.rs	Adds passing enum-binder coverage.
tests/ui/fail/annot_exists_enum_binder.rs	Adds failing enum-binder coverage.
tests/ui/pass/annot_exists_tuple_binder.rs	Adds passing tuple-binder coverage.
tests/ui/fail/annot_exists_tuple_binder.rs	Adds failing tuple-binder coverage.

Review details

• Files reviewed: 9/9 changed files
• Comments generated: 1
• Review effort level: Balanced

---

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