Incompleteness: a `&mut` into an `enum`/`Option` whose payload is a `Vec` (any `Seq`-modeled container) defeats the default solver configuration — a five-line `Option<Vec<i64>>` program times out, while the same code with the container in a struct field, or moved out by value, verifies in 0.5 s

[coord-e]

Summary

Storing a container behind an enum — Option<Vec<T>>, enum State { Buffered(Vec<u8>), … } — and mutating it in place through match &mut e is one of the most common shapes in real Rust. Thrust cannot verify it: a five-line program that pushes two elements into an Option<Vec<i64>> and reads them back reports verification error: Timeout(30s), and is still unsolved after 300 s.

The property is not hard, and the program is not unusual. Three one-word variations of the same program each verify in ~0.5 s:

• put the Vec in a struct field instead of an enum payload — 0.5 s;
• keep the Option but move the payload out by value (match o { Some(mut v) => { v.push(x); Some(v) } … }) — 0.5 s;
• keep match &mut o but make the payload a scalar (Option<i64>) — 0.4 s.

Only the combination mutable borrow × enum payload × Seq-modeled payload fails. In sort terms, the systems that solve instantly carry Mut<Seq<Int>> or Mut<Option<Int>> predicate arguments; the one that hangs is the only one that carries Mut<Option<Seq<Int>>> — a Mut over a datatype whose payload holds an SMT Array.

The failure is two-sided: the buggy variant of the same program (assert!(v.len() == 3)) also times out, so Thrust returns no verdict at all rather than falling back to a correct rejection.

Reproduction

A — control: the container in a struct field (struct_field.rs) — 0.5 s, safe

struct W { v: Vec<i64> }
impl thrust_models::Model for W { type Ty = Self; }

#[thrust::callable]
fn check(x: i64, y: i64) {
    let mut w = W { v: Vec::new() };
    w.v.push(x);
    w.v.push(y);
    assert!(w.v.len() == 2);
    assert!(w.v[0] == x);
    assert!(w.v[1] == y);
}
fn main() {}

B — the repro: the same container in an Option (option_payload.rs) — Timeout(30s)

#[thrust::callable]
fn check(x: i64, y: i64) {
    let mut o: Option<Vec<i64>> = Some(Vec::new());
    match &mut o { Some(v) => v.push(x), None => {} }
    match &mut o { Some(v) => v.push(y), None => {} }
    match o {
        Some(v) => {
            assert!(v.len() == 2);
            assert!(v[0] == x);
            assert!(v[1] == y);
        }
        None => assert!(false),
    }
}
fn main() {}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false option_payload.rs
error: verification error: Timeout(30s)

error: aborting due to 1 previous error

It is not a budget problem: THRUST_SOLVER_TIMEOUT_SECS=300 still times out.

C — workaround: same Option, payload moved out by value (option_byvalue.rs) — 0.5 s, safe

#[thrust::callable]
fn check(x: i64, y: i64) {
    let o: Option<Vec<i64>> = Some(Vec::new());
    let o1 = match o { Some(mut v) => { v.push(x); Some(v) } None => None };
    let o2 = match o1 { Some(mut v) => { v.push(y); Some(v) } None => None };
    match o2 {
        Some(v) => { assert!(v.len() == 2); assert!(v[0] == x); assert!(v[1] == y); }
        None => assert!(false),
    }
}
fn main() {}

A user-defined enum is worse than Option: with enum E { Empty, Items(Vec<i64>) }, one push already exceeds the budget (112 s of solving).

enum E { Empty, Items(Vec<i64>) }
impl thrust_models::Model for E { type Ty = Self; }

#[thrust::callable]
fn check(x: i64) {
    let mut e = E::Items(Vec::new());
    match &mut e {
        E::Items(v) => v.push(x),
        E::Empty => {}
    }
    match e {
        E::Items(v) => { assert!(v.len() == 1); assert!(v[0] == x); }
        E::Empty => assert!(false),
    }
}
fn main() {}

Evidence matrix

All at -Adead_code -C debug-assertions=false, z3 5.0.0, default THRUST_SOLVER_ARGS, wall-clock of the whole thrust-rustc run. "verdict" is under the default 30 s budget; the time column is the run under a 300 s budget where that differs.

program	container lives in	borrow	payload observed	time	verdict (30 s)
bare Vec<i64> local, 2 pushes	—	—	len + both elements	0.4 s	safe
A struct W { v: Vec<i64> }, 2 pushes	struct field	&mut (implicit)	len + both elements	0.5 s	safe
Option<i64>, write then read back	enum payload	match &mut o	the scalar	0.4 s	safe
Option<Vec<i64>>, 1 push	enum payload	match &mut o	len only	1.3 s	safe
Option<Vec<i64>>, 1 push	enum payload	match &mut o	len + v[0]	24 s	safe (borderline)
B Option<Vec<i64>>, 2 pushes	enum payload	match &mut o	len + both elements	>300 s	Timeout(30s)
B with a wrong assertion (len == 3)	enum payload	match &mut o	len	>30 s	Timeout(30s)
C Option<Vec<i64>>, 2 pushes, by value	enum payload	none (moved out)	len + both elements	0.5 s	safe
enum E { Empty, Items(Vec<i64>) }, 1 push	enum payload	match &mut e	len + v[0]	112 s	Timeout(30s)
same via fn add(e: &mut E, x: i64)	enum payload	match &mut e	len + v[0]	114 s	Timeout(30s)
same but fn add(o: &mut Option<Vec<i64>>, x: i64)	enum payload	match &mut o	len + v[0]	149 s	Timeout(30s)

Two rows are worth calling out. The len only row shows the cost is not the enum match by itself — it is reasoning about the container's contents once they have travelled through the enum. And the wrong assertion row shows the failure is two-sided, unlike #243: Thrust no longer even rejects the unsafe program.

Root cause

The distinguishing sort is Mut<Enum<… Seq …>>

Dumping with THRUST_OUTPUT_DIR and listing the Mut sorts each system declares:

program	Mut sorts in the emitted SMT-LIB	result
A (struct field)	Mut<Tuple<Array<Int-Int>-Int>>	0.5 s
Option<i64>	Mut<Int>, Mut<std.option.Option<Int>>	0.4 s
B (Option<Vec<i64>>)	Mut<Tuple<Array<Int-Int>-Int>>, Mut<std.option.Option<Tuple<Array<Int-Int>-Int>>>	hangs

Mut over a Seq alone is affordable (row A). Mut over an enum with a scalar payload is affordable (row 2). Mut over an enum whose payload is Seq-modeled is not.

Why the enum, and not the struct

A struct is elaborated to a tuple, so w.v is a projection: the Vec reaches the predicate as one Tuple<Array,Int> argument and nothing else.

An enum is expanded instead (Env::bind_enum, src/refine/env.rs:737-…): for every variant it allocates a temp per field, recursively bind_impls it, and reconstructs the enum value with a matcher_pred atom. For Option<Seq<Int>> each binding therefore materialises the discriminant, the Seq as a Tuple<Array,Int> datatype, and — because bind_tuple decomposes it further — the Array and the length separately; var_type then rebuilds the enum term from those parts. Every one of them is a live local, so every downstream basic-block predicate carries all of them. In B the widest predicate has 20 arguments, of which 4 are raw (Array Int Int) and 5 are datatypes containing an array; the largest clause quantifies 112 variables (A: 15 arguments, 96 variables). The matcher_pred for that sort is a disjunction over array-carrying constructors:

(define-fun matcher_pred<A2_std.option.Option<Tuple<Array<Int-Int>-Int>>>
    ((x0 A0_Tuple<Array<Int-Int>-Int>) (v A2_std.option.Option<Tuple<Array<Int-Int>-Int>>)) Bool
  (or (= v std.option.Option.None<Tuple<Array<Int-Int>-Int>>)
      (= v (std.option.Option.Some<Tuple<Array<Int-Int>-Int>> x0))))

so each match adds a case split over equalities between datatypes that contain arrays, and the &mut adds a second copy of all of it for the prophecy.

Enum expansion depth is not the driver: THRUST_ENUM_EXPANSION_DEPTH_LIMIT of 3 or 4 gives the same times as the default 2 (and 1 makes the repro ICE, cf. #253).

The system is acyclic, and z3's eager Horn inlining is what diverges

Parsing B's 28 clauses and building the body → head predicate dependency graph gives no cycles at all. There is no user-written un-annotated helper and no loop; Vec::push carries an extern spec, so it contributes no template.

Feeding B's dump straight to z3:

$ z3 fp.spacer.global=true fp.validate=true thrust_output.smt2   # what Thrust passes today
(no answer in 90 s)
$ z3 thrust_output.smt2                                          # z3 defaults
(no answer in 90 s)
$ z3 fp.xform.inline_eager=false thrust_output.smt2
sat                                                              # 5.4 s

End to end, with THRUST_SOLVER_ARGS="fp.spacer.global=true fp.validate=true fp.xform.inline_eager=false":

program	default args	+ fp.xform.inline_eager=false
B (Option<Vec<i64>>, 2 pushes)	Timeout(30s)	safe, 7.1 s
enum E, 1 push, inline	Timeout(30s)	safe, 1.1 s
enum E, 1 push, via fn add(&mut E, i64)	Timeout(30s)	safe, 2.4 s

Relation to #243

#243 reaches the same z3 option from a different program shape, and its model does not cover this one. It concludes that "ADT-sorted predicate arguments are affordable, and recursive templates are affordable, but not together", with the recursion coming from one inference template reused at two call sites of an un-annotated &mut-taking helper — and it notes that "v.push(x)-style code is unaffected because the Vec methods carry extern specs".

This repro has no recursion (the dependency graph is acyclic), no un-annotated helper (variant B is helper-free; the helper variants behave the same), and no &mut parameter (check takes two i64s). It is v.push(x)-style code. So ingredient 1 of #243 is absent and ingredient 2 alone suffices, once the ADT payload carries an Array. #243's suggested fix — representing a &mut T parameter by its two scalar components — would not reach this case either: the Mut here is created by match &mut o on a local, and its referent is an enum, not a scalar.

(As a caveat in the other direction: the two Sink-style variants I tried, where an un-annotated fn write(&mut self, x: i64) is called twice, time out even with the container directly in a struct field, i.e. they are #243 and not this issue. The rows in the matrix above are all helper-free or single-call.)

Suggested direction

Attack the encoding rather than the solver flag — as #243 records, fp.xform.inline_eager=false regresses tests/ui/{pass,fail}/iterators/fixed_filter_*.rs from correct to Timeout, so it is a diagnostic, not a patch.

Two candidates, in rough order of appeal:

1. Do not re-materialise an enum's payload when it is already flow-bound. bind_enum allocates a fresh field temp for every variant on every binding, and the same enum-valued local ends up constrained by several identical matcher_pred atoms in one clause (in B's largest clause, six distinct groups of components are each duplicated 2–4×). Reusing the existing binding would cut the array-sorted argument count roughly in half before anything else changes.
2. Keep Seq-modeled payloads out of datatype arguments. A Vec behind an enum reaches the predicates as Option<Tuple<Array,Int>>; passing the payload's (Array, Int) components alongside the discriminant instead — which is what the struct-field elaboration effectively already does, and what makes row A fast — would make the enum system structurally similar to the struct one.

Environment

• thrust @ 2bf022d
• rustc nightly-2025-09-08 (per rust-toolchain.toml), edition-2015 default and --edition=2021 behave identically here
• Z3 5.0.0 (x64-glibc-2.39, the version .github/actions/setup-z3 pins), default THRUST_SOLVER_ARGS, default 30 s timeout

[coord-e]

The enum is not the trigger — it is a constant factor on an exponential that a bare Vec local is already on

Same root cause as this issue (array-carrying datatype arguments in the predicate chain, same fp.xform.inline_eager signature), but the scope is much wider than the report states, and the three rows this issue uses as controls are not controls — they are the same curve sampled at n = 2.

Cost multiplies ~3.5× per Seq-carrying operation in straight-line code. No enum, no Option, no &mut parameter, no un-annotated helper, no loop, no recursion needed. A bare Vec<i64> local with 16 pushes and nothing else is already unverifiable.

Repro — 18 lines, Timeout(30s)

fn main() {
    let mut v: Vec<i64> = Vec::new();
    v.push(0);
    v.push(1);
    v.push(2);
    v.push(3);
    v.push(4);
    v.push(5);
    v.push(6);
    v.push(7);
    v.push(8);
    v.push(9);
    v.push(10);
    v.push(11);
    v.push(12);
    v.push(13);
    v.push(14);
    v.push(15);
    assert!(v.len() == 16);
}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro16.rs
error: verification error: Timeout(30s)

Still Timeout at THRUST_SOLVER_TIMEOUT_SECS=300. The emitted system is 23 predicates / 22 clauses.

The curve

v.push(i) repeated n times in main, wall-clock of the whole thrust-rustc run, 300 s budget:

pushes	2	4	6	8	10	12	13	14	15	16
time	0.28 s	0.33 s	0.31 s	0.46 s	0.72 s	3.56 s	11.2 s	41.6 s	164 s	>300 s

Clean ×3.5–4 per push once it leaves the floor. Nothing in the program changes shape; only the count does.

The three "controls" in the report are on the same curve

Row A, struct W { v: Vec<i64> } — reported here as 0.5 s and used as evidence that the enum is what costs. Scaled up, it is indistinguishable from the bare local:

pushes into w.v	2	8	10	12	14
time	0.25 s	0.39 s	0.70 s	3.44 s	42.0 s

Row C, payload moved out by value — reported as the workaround. A Vec threaded by value through an annotated helper (#[ensures(result.length == v.length)] fn f(v: Vec<i64>) -> Vec<i64> { v }) called n times:

calls	4	8	10	12	14
time	0.29 s	0.40 s	0.78 s	4.91 s	Timeout(60s)

Row B, Option<Vec<i64>> via match &mut o — for comparison on the same build: 1 push 0.93 s, 2 pushes >120 s.

So all three shapes are the same exponential; the container only sets the base. Bare local and struct field: ~×3.5 per operation from a 0.25 s floor, cliff at n ≈ 15. Option payload: ~×130 per operation, cliff at n = 2. The enum expansion makes each step far more expensive — which is what this issue measured — but removing it only moves the cliff, it does not remove it.

It is not the store chain, and not program size

Reads alone are enough. One v.push(0), then n times let b: usize = v.len(); — nothing is mutated, the array term never grows:

v.len() reads	8	12	14	16
time	0.41 s	10.2 s	Timeout(120s)	Timeout(120s)

So it is not reasoning about array contents; merely carrying the Seq value through n clauses is what costs.

Program length is free when the sort is scalar. Each of these is flat where the Vec versions are dead — n here is the same statement count:

shape	n = 16	n = 20	n = 40	n = 100
a = a + i;	0.24 s	—	0.26 s	0.30 s
if a > i { .. } else { .. } chain	0.34 s	—	—	—
s.a = s.a + i; (struct field)	0.25 s	—	—	—
p = f(p) , f: (i64,i64) -> (i64,i64), annotated	0.39 s	1.12 s	—	—
s = f(s, i), f: P -> P (model struct, inferred spec)	0.43 s	5.06 s	—	—
f(&mut s, i), f: &mut P, annotated	0.45 s	1.22 s	—	—
a = f(a, i), f: (i64,i64) -> i64 (inferred spec)	0.45 s	3.72 s	—	—

Datatype-sorted predicate arguments in general are fine — tuples, model structs, even Mut<Tuple<Int,Int>>. Only the array-carrying Seq is not.

A loop is free. The same pushes under an invariant! are summarised by one predicate and never build a chain:

fn main() {
    let mut v: Vec<i64> = Vec::new();
    let mut i: i64 = 0;
    while i < 100 {
        thrust_macros::invariant!(|i: i64, v: Vec<i64>| v.length >= 0);
        v.push(i);
        i += 1;
    }
    assert!(v.len() >= 0);
}

0.26 s at bound 100, versus >300 s for 16 unrolled pushes. It is straight-line repetition that dies, which is the shape hand-written code actually has.

Structural reason: block preconditions accumulate, so the chain is non-linear and grows

The dump for the 16-push repro, body predicate atoms per clause:

c0: 1   c1: 2   c2: 3   c3: 4   c4: 5   c5: 6   c6: 7   c7: 8   c8: 9
c9: 10  c10: 11 c11: 12 c12: 13 c13: 14 c14: 15 c15: 16 c16: 17 c17: 18
c18: 19 c19: 18 c20: 1  c21: 0

Clause k conjoins every preceding block predicate, not just its immediate predecessor:

; c1
(=> (and p3 p4 ...) (p5 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9))
; c2
(=> (and p5 p3 p4 ...) (p6 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9))
; c3
(=> (and p6 p5 p3 p4 ...) (p7 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9))

Every one of those atoms carries the Tuple<Array<Int-Int>-Int> / Mut<Tuple<Array<Int-Int>-Int>> arguments. This growing conjunction is emitted for scalar programs too (the a = f(a, i) chain above has the identical atom-count profile) — it is affordable there and unaffordable once the arguments carry an Array, which is why the split falls exactly along the sort and not along the program shape.

Two-sided, same as row B

14 pushes with a deliberately wrong assertion (assert!(v.len() == 15)) also times out at 120 s. Past the cliff Thrust returns no verdict in either direction.

Same solver signature

$ THRUST_SOLVER_ARGS="fp.spacer.global=true fp.validate=true fp.xform.inline_eager=false" \
    cargo run -q -- -Adead_code -C debug-assertions=false repro16.rs && echo safe
safe            # 2.4 s, vs Timeout(30s) with the defaults

Feeding the dump straight to z3: default args no answer in 100 s, fp.xform.inline_eager=false → sat in 0.09 s. Consistent with what #243 and this issue both found, and with the same caveat — it regresses tests/ui/{pass,fail}/iterators/fixed_filter_*.rs, so it stays a diagnostic.

What this changes about the suggested direction

Suggested fix 1 here ("do not re-materialise an enum's payload when it is already flow-bound") would halve the array-sorted argument count in the Option case and so move its cliff from n = 2 to somewhere around n = 4–6 — real progress for that shape, but the bare-local and struct-field programs never had an enum to fix and still die at n ≈ 15.

Suggested fix 2 ("keep Seq-modeled payloads out of datatype arguments") is aimed the right way but its stated target is the enum case, and the justification given for it — that the struct-field elaboration "is what makes row A fast" — does not hold: row A is fast only at n = 2. What the data points at is the combination of (a) the accumulating, non-linear block-precondition chain above and (b) Seq values reaching predicates as array-carrying datatype arguments. Either one alone is affordable. Making each block's precondition depend only on its immediate predecessor would bound the body size independently of the sort, and would help every shape in this issue including the enum one.

Might be worth re-scoping/retitling this issue away from enum/Option, since the enum turns out to be an amplifier rather than the trigger.

How this turned up

Random straight-line programs over &mut/Vec/Option/model structs and enums, checked against real rustc for ground truth: 239 programs, zero soundness or completeness mismatches — every verdict Thrust returned was correct — but 46 of them (19%) returned no verdict at all, all of them solver timeouts of this kind. On this corpus timeouts are the only failure mode left.

Environment

• thrust @ 2bf022d (same commit as this issue)
• rustc nightly-2025-09-08 (per rust-toolchain.toml), --edition 2021
• Z3 5.0.0 (x64-glibc-2.39, the version .github/actions/setup-z3 pins), default THRUST_SOLVER_ARGS
• Timeouts noted per table (30 s default, or 120 s / 300 s where stated)

---

Generated by Claude Code