Summary

Env::dropping_formula_for_term (src/refine/env.rs) recurses infinitely and overflows the stack when analyzing a recursive enum whose recursive Box<Self> (or &mut Self) is reached through a tuple/struct field instead of being a direct field of the variant. The recursive-ADT cutoff only recognizes a direct pointer field, so any indirection bypasses it.

This needs no mutable references — a purely-owned recursive data type triggers it — and the program being analyzed is trivially safe.

Reproduction (minimal)

enum L { Cons((i64, Box<L>)), Nil }   // recursive Box<L> nested in a tuple field
impl thrust_models::Model for L { type Ty = Self; }

#[thrust::callable]
fn check() {
    let l = L::Cons((1, Box::new(L::Nil)));
    assert!(matches!(l, L::Cons(_)));   // trivially true
}
fn main() {}

$ THRUST_SOLVER=z3 cargo run -q -- -Adead_code -C debug-assertions=false repro.rs
thread 'rustc' has overflowed its stack
fatal runtime error: stack overflow, aborting
(exit 134)

The direct form — where the recursive Box<L> is a direct field of the variant — verifies cleanly:

enum L { Cons(i64, Box<L>), Nil }     // direct recursive field
impl thrust_models::Model for L { type Ty = Self; }
#[thrust::callable]
fn check() {
    let l = L::Cons(1, Box::new(L::Nil));
    assert!(matches!(l, L::Cons(_, _)));   // verifies: exit 0
}
fn main() {}

So the only difference between "crashes" and "verifies" is whether the recursive pointer sits directly in the variant or inside a tuple field of the variant.

Mechanism

src/refine/env.rs, dropping_formula_for_term (~lines 1120-1166). The three relevant branches:

} else if ty.is_own() {                                   // (A) Box: recurse into pointee
    let inner = &ty.as_pointer().unwrap().elem.ty;
    self.dropping_formula_for_term(existentials, inner, term.box_current())
} else if let Some(tty) = ty.as_tuple() {                 // (B) tuple: recurse into each element
    ...
    self.dropping_formula_for_term(existentials, &elem.ty, term.clone().tuple_proj(i))
    ...
} else if let Some(ety) = ty.as_enum() {                  // (C) enum: recurse into each variant field
    ...
    for field_ty in enum_def.field_tys() {
        ...
        if let Some(p) = field_type.as_pointer() {
            if matches!(&p.elem.ty, rty::Type::Enum(e) if e.symbol == ety.symbol) {
                // TODO: we need recursively defined drop_pred for the recursive ADTs!
                tracing::warn!("skipping recursive variant");
                continue;                                  // <-- the ONLY cycle cutoff
            }
        }
        self.dropping_formula_for_term(existentials, &field_type, field_term);
    }
    ...
}

The cycle cutoff in branch (C) engages only when a variant field's type is itself a pointer to the same enum (field_type.as_pointer() → Enum(e) with the same symbol). For Cons((i64, Box<L>)) the field type is a tuple, so the as_pointer() check fails and the guard is skipped. The descent then goes:

enum L (C) → tuple (i64, Box<L>) (B) → Box<L> (A) → enum L (C) → tuple … (B) → Box<L> (A) → …   ∞

Neither the tuple branch (B) nor the owned-pointer branch (A) has any cycle guard of its own, so the recursion never terminates. The TODO on line 1151 already flags that the current cutoff is a stopgap ("we need recursively defined drop_pred for the recursive ADTs"); this report is a concrete case where the stopgap is bypassed entirely and turns into a hard crash rather than a skipped obligation.

Notes

• Valid, safe Rust: the reproducer compiles and runs fine under rustc; the assert! is always true.
• Distinct from the recursive-ADT prophecy issues (Incompleteness: dropping a recursively-defined ADT does not resolve &mut prophecies stored in its recursive-position field, so safe programs are wrongly rejected #173 wrong-verdict for &mut in a recursive-position field; Incompleteness: a &mut stored in a Box has its prophecy resolved only at the Box's drop, so reading the referent before the box is dropped wrongly rejects safe programs #175 Box-held &mut prophecy timing): this reproducer contains no &mut at all, and the symptom is non-termination / stack overflow, not a wrong soundness/completeness verdict. It is triggered purely by the shape of the owned recursive type during drop-formula construction.
• Any indirection through an aggregate should reproduce it (e.g. a struct field wrapping the Box<L>), since the guard is keyed on a direct pointer field.

Environment

• thrust @ af7cd99 (current main)
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• z3 4.16.0