Quantifier (`forall`/`exists`) binder sorts are never declared in SMT-LIB, so any spec quantifying over a datatype/tuple-sorted variable emits an undefined sort

[coord-e]

Summary

collect_sorts (src/chc/format_context.rs:209-225) gathers the sorts that need datatype declarations in the emitted SMT-LIB only from (a) pred_vars signatures, (b) clause.vars, and (c) the argument terms of atoms (via atom_sorts/term_sorts). It never visits the binder sorts of Formula::Exists / Formula::Forall. Compounding this, term_sorts ignores the sort carried by a quantified variable term:

// src/chc/format_context.rs:60
chc::Term::FormulaQuantifiedVar(_, _) => {}

As a result, when a forall/exists quantifies over a variable whose sort is a datatype, tuple, or any other non-builtin/composite sort that does not otherwise appear in the same clause, that sort is never collected, so no declare-datatype is emitted for it. The generated SMT then references an undeclared sort inside the quantifier, and any SMT solver rejects the query as ill-typed.

This is an incompleteness bug, not a soundness hole: the malformed SMT is rejected at parse time (before solving), surfaced as a generic verification error, so safe programs are falsely rejected rather than wrongly accepted. Because it fails during SMT parsing, it is independent of which CHC backend is used — the PCSat solver normally required for quantified specs would reject it just the same.

Reproduction

repro.rs — a postcondition that quantifies over an enum-sorted variable:

//@compile-flags: -C debug-assertions=off
use thrust_models::exists;

enum E {
    A(i32),
    B,
}

#[thrust_macros::ensures(exists(|e: E| result >= 0))]
fn f() -> i32 {
    0
}

fn main() {}

$ THRUST_OUTPUT_DIR=/tmp/out cargo run -q -- -Adead_code -C debug-assertions=false repro.rs
error: verification error: Error { stdout: "(error \"line 19 column 85: invalid sorted variables: unknown sort 'E'\")\nsat\n", stderr: "" }

The generated /tmp/out/thrust_output.smt2 uses E in the quantifier binder but never declares it (no declare-datatype for E anywhere in the file):

(assert (forall ((v0 Int) (v1 Int))
  (=> (and (= v0 0) p4 (= v1 v0) (not (exists ((e E)) (>= v1 0)))) false)))

The body need not even reference the bound variable — and referencing it does not help, because term_sorts drops the sort of a FormulaQuantifiedVar (line 60 above) and DatatypeCtor only recurses into its arguments without adding its own datatype sort.

Also reproduces for tuple-sorted binders

use thrust_models::exists;
#[thrust_macros::ensures(exists(|p: (i32, i32)| result >= 0))]
fn f() -> i32 { 0 }
fn main() {}

error: verification error: Error { stdout: "(error \"line 19 column 85: invalid sorted variables: unknown sort 'Tuple<Int-Int>'\")\nsat\n", stderr: "" }

with the emitted assert containing (exists ((p Tuple<Int-Int>)) ...) and zero declare-datatype.

Control: the sort is declared when it appears outside the quantifier

Adding a parameter of the same sort makes E reach clause.vars, so it is collected and declared, and the unknown sort error disappears:

use thrust_models::exists;
enum E { A(i32), B }
#[thrust_macros::ensures(exists(|e: E| result >= 0))]
fn f(used: E) -> i32 { 0 }   // `used: E` => E now appears as a clause var
fn main() {}

This isolates the defect to quantifier-binder-only sorts.

Root cause

src/chc/format_context.rs:

fn collect_sorts(system: &chc::System) -> BTreeSet<chc::Sort> {
    let mut sorts = BTreeSet::new();
    for def in &system.pred_vars {
        sorts.extend(def.sig.clone());
    }
    for clause in &system.clauses {
        sorts.extend(clause.vars.clone());
        atom_sorts(clause, &clause.head, &mut sorts);
        for a in clause.body.iter_atoms() {        // walks atoms, but NOT quantifier binders
            atom_sorts(clause, a, &mut sorts);
        }
    }
    sorts
}

iter_atoms() (src/chc.rs:1504-1506) does descend into Exists/Forall bodies, so atoms inside a quantifier are visited — but the binder list Vec<(String, Sort)> is metadata that no atom references, and term_sorts discards the sort of the only term that mentions a bound variable (FormulaQuantifiedVar). So a binder-only sort is invisible to collect_sorts, hence never declared by FormatContext::from_system (format_context.rs:263-280).

Expected behavior / fix direction

collect_sorts must also collect the sorts of Exists/Forall binders (and, defensively, the sort of FormulaQuantifiedVar in term_sorts). Concretely, walk the formula structure of clause.head/clause.body and, for each Formula::Exists(vars, _) / Formula::Forall(vars, _), sorts.extend(vars.iter().map(|(_, s)| s.clone())), and change the FormulaQuantifiedVar(sort, _) arm of term_sorts to insert sort. Either change alone fixes the binder case; doing both is robust. (Composite binder sorts then also need their monomorphized/builtin datatype declarations, which from_system already derives from the collected sort set, so collecting the sort is sufficient.)

Related but distinct

• Undefined sort name in SMT2 when predicate argument is a struct containing a closure #47 ("Undefined sort name in SMT2 when predicate argument is a struct containing a closure") is also an "undefined sort" symptom, but its cause is the predicate define-fun emitting a Tuple sort for a closure-containing struct argument — a different code path with a different trigger. The bug here is specifically about forall/exists binder sorts in collect_sorts/term_sorts and triggers on plain enums/tuples with no closures or predicates involved.

Environment

• thrust @ 70846d7
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 4.16.0, default solver configuration (THRUST_SOLVER=z3)