Issues

Incompleteness: `v.len()` on a `&mut [T]` leaves an unresolved reborrow that havocs the referent, so every safe `&mut` slice program that guards an index with `len()` is rejected at any `-C opt-level >= 1`

bug

#240

· coord-e opened

on Aug 22, 2026

Implicit derefs (rustc adjustments) are dropped in annotation translation, so any `v.len()`/`v.length`/`s.0` on a `&mut` parameter builds an ill-sorted term and ICEs — only the explicit `(*v)` spelling works

bug

#239

· coord-e opened

on Aug 21, 2026

Incompleteness: `#[requires(..)]` alone pins the postcondition to `true` instead of leaving it inferred (unlike `closure!(requires(..))` and `#[param(..)]`), so adding a precondition silently strips every caller of the call's result

bug

#238

· coord-e opened

on Aug 20, 2026

Incompleteness: a local `impl PartialEq` is checked against the blanket `_extern_spec_partialeq_eq` (structural model equality), so any non-structural `eq` — even one that is never used — makes the whole crate fail with `Unsat`

bug

#225

· coord-e opened

on Aug 15, 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

Navigation Menu

All issues

Incompleteness: `v.len()` on a `&mut [T]` leaves an unresolved reborrow that havocs the referent, so every safe `&mut` slice program that guards an index with `len()` is rejected at any `-C opt-level >= 1`

Implicit derefs (rustc adjustments) are dropped in annotation translation, so any `v.len()`/`v.length`/`s.0` on a `&mut` parameter builds an ill-sorted term and ICEs — only the explicit `(*v)` spelling works

Incompleteness: `#[requires(..)]` alone pins the postcondition to `true` instead of leaving it inferred (unlike `closure!(requires(..))` and `#[param(..)]`), so adding a precondition silently strips every caller of the call's result

Incompleteness: a local `impl PartialEq` is checked against the blanket `_extern_spec_partialeq_eq` (structural model equality), so any non-structural `eq` — even one that is never used — makes the whole crate fail with `Unsat`

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`

Search results