Issues

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

#221

· coord-e opened

on Aug 14, 2026

Unsound: a user `Drop` impl is never checked at the drop site — `TerminatorKind::Drop` only resolves prophecies, so a destructor that panics verifies as `safe`

bug

#215

· coord-e opened

on Aug 13, 2026

Unsound: `==` on `&mut` references compares the prophecy too, so the comparison's result depends on writes made after it — panicking programs verify as `safe`

bug

#210

· coord-e opened

on Aug 10, 2026

Unsound: a two-phase borrow (`v.push(v.len())`) havocs the receiver before the arguments are evaluated, so reads in the argument see the prophecy — panicking programs verify as `safe`

#209

· coord-e opened

on Aug 9, 2026

Unsound: moving a `&mut`-capturing closure out of any aggregate (incl. `enum`/`Option`), with no higher-order call, drops its prophecy and verifies panicking programs as `safe` (generalizes #177)

bug

#207

· coord-e opened

on Aug 8, 2026

Incompleteness: an explicit `invariant!` on a loop that writes through a `&mut` drops the reference's prophecy link, so the referent is havoc'd after the borrow ends — safe programs wrongly rejected (no workaround; the inference path handles it)

#205

· coord-e opened

on Aug 6, 2026

Unsound: `Vec` equality (`==`) is modeled as structural equality of the whole `(array, length)` representation, so vectors equal in Rust but differing in stale slots past `length` (after `pop`/`truncate`) compare unequal — dead-branch panics verify as `safe`

bug

#203

· coord-e opened

on Aug 5, 2026

Incompleteness: a `&mut` stored in a `Vec` (Seq/array-backed container) never has its prophecy resolved at drop, so safe programs are wrongly rejected as `Unsat`

#202

· coord-e opened

on Aug 3, 2026

Incompleteness: a `fn(..)` pointer value called outside the basic block that created it loses the callee's refinement spec (result is havoc'd), so valid programs verify as `Unsat`

#201

· coord-e opened

on Aug 2, 2026

Unsound: an uncalled generic function (a type param appears in its signature) has its body skipped entirely, so a `#[thrust::callable]` entry point whose body always panics — or whose body violates its own `ensures` — verifies as `safe`

#200

· coord-e opened

on Aug 1, 2026

`thrust-rustc` compiles at rustc's default edition (2015), not 2021 like its `ui_test` suite: annotation diagnostics are masked as `E0433: missing crate 'core'`, and edition-sensitive programs behave differently

#199

· coord-e opened

on Jul 31, 2026

Unsound: a `#[param(name: { v | φ })]` precondition combined with `#[ensures(..)]` is dropped at call sites too, so a `#[thrust::trusted]` function with a violated precondition verifies panicking programs as `safe`

#196

· coord-e opened

on Jul 28, 2026

Navigation Menu

All issues

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

Unsound: a user `Drop` impl is never checked at the drop site — `TerminatorKind::Drop` only resolves prophecies, so a destructor that panics verifies as `safe`

Unsound: `==` on `&mut` references compares the prophecy too, so the comparison's result depends on writes made after it — panicking programs verify as `safe`

Unsound: a two-phase borrow (`v.push(v.len())`) havocs the receiver before the arguments are evaluated, so reads in the argument see the prophecy — panicking programs verify as `safe`

Unsound: moving a `&mut`-capturing closure out of any aggregate (incl. `enum`/`Option`), with no higher-order call, drops its prophecy and verifies panicking programs as `safe` (generalizes #177)

Incompleteness: an explicit `invariant!` on a loop that writes through a `&mut` drops the reference's prophecy link, so the referent is havoc'd after the borrow ends — safe programs wrongly rejected (no workaround; the inference path handles it)

Unsound: `Vec` equality (`==`) is modeled as structural equality of the whole `(array, length)` representation, so vectors equal in Rust but differing in stale slots past `length` (after `pop`/`truncate`) compare unequal — dead-branch panics verify as `safe`

Incompleteness: a `&mut` stored in a `Vec` (Seq/array-backed container) never has its prophecy resolved at drop, so safe programs are wrongly rejected as `Unsat`

Incompleteness: a `fn(..)` pointer value called outside the basic block that created it loses the callee's refinement spec (result is havoc'd), so valid programs verify as `Unsat`

Unsound: an uncalled generic function (a type param appears in its signature) has its body skipped entirely, so a `#[thrust::callable]` entry point whose body always panics — or whose body violates its own `ensures` — verifies as `safe`

`thrust-rustc` compiles at rustc's default edition (2015), not 2021 like its `ui_test` suite: annotation diagnostics are masked as `E0433: missing crate 'core'`, and edition-sensitive programs behave differently

Unsound: a `#[param(name: { v | φ })]` precondition combined with `#[ensures(..)]` is dropped at call sites too, so a `#[thrust::trusted]` function with a violated precondition verifies panicking programs as `safe`

Search results