Panic / undeclared SMT sort: an enum reachable only through an ADT's field type is never registered in `EnumDefs`, so any struct with an enum-typed field (`struct W { o: Option<i32> }`) aborts verification

[coord-e]

Summary

basic_block::Analyzer::register_enum_defs (src/analyze/basic_block.rs:1328) discovers the enums a body needs by running a TypeVisitor over the types of the MIR local declarations. TypeVisitor::super_visit_with on an Adt descends only into that ADT's generic arguments — it never looks at the ADT's field types. So an enum that occurs only as a field type of another struct/enum, and that never appears as the type of some local in the body, is never passed to get_or_register_enum_def.

refine::Env's EnumDefProvider then fails to find it and unwraps:

// src/analyze.rs:213-216
impl refine::EnumDefProvider for Rc<RefCell<EnumDefs>> {
    fn enum_def(&self, name: &chc::DatatypeSymbol) -> rty::EnumDatatypeDef {
        self.borrow().find_by_name(name).unwrap().clone()   // <-- None
    }
}

The elaboration of an ADT does reach those field types (a struct becomes a tuple of boxed fields, an enum variant's fields are bound individually), so Env::bind_enum / Env::dropping_formula_for_term ask for the missing def and Thrust aborts.

This is not an unsupported construct: the very same enum nesting verifies fine as soon as any local in the body happens to have the inner enum's type (see the control below). It is purely a bookkeeping gap in enum-def registration.

The shape that triggers it is ordinary Rust — a struct with an Option field is enough.

Reproduction 1 — by-value parameter: ICE

ice_by_value.rs:

struct Wrap { o: Option<i32> }

impl thrust_models::Model for Wrap { type Ty = Self; }

#[thrust::callable]
fn f(_w: Wrap) {}

fn main() {}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false ice_by_value.rs

thread 'rustc' (9678) panicked at src/analyze.rs:215:42:
called `Option::unwrap()` on a `None` value
stack backtrace:
   ...
   4: core::option::Option<T>::unwrap
   5: thrust::analyze::<impl thrust::refine::env::EnumDefProvider for alloc::rc::Rc<core::cell::RefCell<thrust::analyze::EnumDefs>>>::enum_def
             at /home/user/thrust/src/analyze.rs:215:42
   6: thrust::refine::env::Env<T>::dropping_formula_for_term
             at /home/user/thrust/src/refine/env.rs:1145:43
   7: thrust::refine::env::Env<T>::dropping_formula_for_term
             at /home/user/thrust/src/refine/env.rs:1131:18
   8: thrust::refine::env::Env<T>::dropping_formula_for_term
             at /home/user/thrust/src/refine/env.rs:1135:37
   9: thrust::refine::env::Env<T>::dropping_assumption
             at /home/user/thrust/src/refine/env.rs:1117:32
  10: thrust::refine::env::Env<T>::drop_local
             at /home/user/thrust/src/refine/env.rs:1182:31

A user-defined enum nested in a user-defined enum fails identically:

enum Inner { P(i32), Q }
enum Outer { X(Inner), Y }

impl thrust_models::Model for Inner { type Ty = Self; }
impl thrust_models::Model for Outer { type Ty = Self; }

#[thrust::callable]
fn f(_o: Outer) {}

fn main() {}

…and so does the realistic version of the same program, where the nested pattern is what keeps Inner from ever being a local's type:

enum Inner { P(i32), Q }
enum Outer { X(Inner), Y }

impl thrust_models::Model for Inner { type Ty = Self; }
impl thrust_models::Model for Outer { type Ty = Self; }

fn f(o: Outer) -> i32 {
    match o {
        Outer::X(Inner::P(v)) => v,   // nested pattern: no local of type `Inner`
        Outer::X(Inner::Q) => 1,
        Outer::Y => 2,
    }
}

fn main() { assert!(f(Outer::X(Inner::P(9))) == 9); }

Reproduction 2 — by-reference parameter: undeclared SMT-LIB2 sort

Behind a &, the same missing registration surfaces as a datatype that is used but never declared, and the run dies on a raw solver error instead:

bad_smt.rs:

struct Wrap { o: Option<i32> }

impl thrust_models::Model for Wrap { type Ty = Self; }

#[thrust::callable]
fn f(_w: &Wrap) {}

fn main() {}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false bad_smt.rs
error: verification error: Error { stdout: "(error \"line 3 column 19: invalid datatype declaration, unknown sort 'std.option.Option<Int>'\")\n(error \"line 9 column 116: invalid function declaration reference, unknown function tuple<std.option.Option<Int>>\")\n(error \"line 10 column 64: invalid sorted variables: unknown sort 'std.option.Option<Int>'\")\nsat\n", stderr: "" }

THRUST_OUTPUT_DIR shows the emitted SMT-LIB2 referring to a sort that was never declared, because Option never made it into chc::System::datatypes:

(set-logic HORN)

(declare-datatypes ((A0_Tuple<std.option.Option<Int>> 0)) (
  (par () (
    (tuple<std.option.Option<Int>> (tuple_proj<std.option.Option<Int>>.0 std.option.Option<Int>))
  ))
))

The user-enum variant of this program produces the same thing with unknown sort 'Inner' / unknown function Outer.X.

Control: it is registration, not lack of support

Adding a parameter whose type is the inner enum makes the enum appear in local_decls, so register_enum_defs picks it up and the identical nesting verifies:

enum Inner { P(i32), Q }
enum Outer { X(Inner), Y }

impl thrust_models::Model for Inner { type Ty = Self; }
impl thrust_models::Model for Outer { type Ty = Self; }

#[thrust::callable]
fn f(_o: Outer, _i: Inner) {}   // <-- only difference

fn main() {}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false control.rs && echo 'safe'
safe

Likewise, struct Wrap { o: Option<i32> } verifies fine when the body happens to create an Option<i32> local:

struct Wrap { o: Option<i32> }
impl thrust_models::Model for Wrap { type Ty = Self; }

fn main() {
    let w = Wrap { o: Some(3) };
    match w.o { Some(x) => assert!(x == 3), None => assert!(false) }   // creates an `Option<i32>` local
}

So whether a program is analyzable depends on whether some unrelated local happens to mention the inner enum.

Root cause

src/analyze/basic_block.rs:1328-1351:

fn register_enum_defs(&mut self) {
    for local_decl in &self.local_decls {
        use mir_ty::{TypeSuperVisitable as _, TypeVisitable as _};
        #[derive(Default)]
        struct EnumCollector {
            enums: std::collections::HashSet<DefId>,
        }
        impl<'tcx> mir_ty::TypeVisitor<mir_ty::TyCtxt<'tcx>> for EnumCollector {
            fn visit_ty(&mut self, ty: mir_ty::Ty<'tcx>) {
                if let mir_ty::TyKind::Adt(adt_def, _) = ty.kind() {
                    if adt_def.is_enum() {
                        self.enums.insert(adt_def.did());
                    }
                }
                ty.super_visit_with(self);   // <-- descends into generic args only
            }
        }
        let mut visitor = EnumCollector::default();
        local_decl.ty.visit_with(&mut visitor);
        for def_id in visitor.enums {
            self.ctx.get_or_register_enum_def(def_id);
        }
    }
}

super_visit_with on TyKind::Adt(def, args) visits args, not def's fields. That is why Vec<Inner> or Option<Inner> in a local's type registers Inner (it is a generic argument), while struct Wrap { o: Option<i32> } or enum Outer { X(Inner), Y } does not (it is a field type).

refine::template::TemplateTypeBuilder::build and Analyzer::build_enum_def happily construct rty::EnumType::new(datatype_symbol(..), ..) for those field types without registering them, and Env::bind_enum / Env::dropping_formula_for_term / PlaceType::downcast later resolve the symbol through EnumDefProvider::enum_def, which unwraps.

Confirmation: making the collector also walk adt_def.all_fields() (with a seen set for recursive ADTs) makes both by-value reproductions above verify as safe, with no other change.

Expected behavior

An enum's EnumDatatypeDef should be registered whenever the analyzer builds an rty::EnumType for it, rather than relying on the enum textually occurring in a local declaration's type. Either

• have register_enum_defs follow ADT field types transitively (guarding against recursive ADTs), or
• register lazily at the point where refine::datatype_symbol / rty::EnumType::new is used to build the type (which also fixes build_enum_def, whose TypeBuilder currently has no access to the registry and so cannot register the enums it discovers in variant field types).

Independently, EnumDefProvider::enum_def returning Option and letting callers report a diagnostic would turn the remaining gaps into errors rather than an ICE.

Relation to existing issues

• Undefined sort name in SMT2 when predicate argument is a struct containing a closure #47 also reports an undefined sort name in the emitted SMT2, but for a predicate argument that is a struct containing a closure; the cause here is a missing declare-datatypes entry for an enum, and it reproduces with no closures and no predicates.
• Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field #178 / Incompleteness: dropping a recursively-defined ADT does not resolve &mut prophecies stored in its recursive-position field, so safe programs are wrongly rejected #173 concern recursive ADTs in dropping_formula_for_term; this one needs no recursion — Inner and Outer (or Wrap and Option) are distinct, non-recursive types.
• Unsound: enum variants after an explicit discriminant get the wrong datatype_discr value, making match arms vacuously verify #126 / Unsound: negative SwitchInt match targets are sign-truncated to large positives, making match arms verify under a wrong path assumption #132 are wrong-value bugs in discriminant handling; this is a missing registration and always aborts (never returns a wrong safe).

Environment

• thrust @ cbc7d3e
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0 (the version .github/actions/setup-z3 pins), default solver configuration