Search results

Incompleteness: a refinement on a generic type argument in #[param] position is dropped for multi-variant enums, so the payload refinement is never assumed in the callee

bugSomething isn't workingSomething isn't working

Status: Open.

#193 In coord-e/thrust;

· coord-e opened on Jul 26, 2026

Incompleteness: an existentially-quantified precondition (requires(exists ..)) emits a quantifier into the Horn clause body, so the default z3 solver returns unknown — Result::unwrap/unwrap_err are unverifiable

Status: Open.

#192 In coord-e/thrust;

· coord-e opened on Jul 25, 2026

Incompleteness: a #[param(name: { v | φ })] precondition is silently dropped when the function also has an #[ensures(..)], so trivially-correct functions are rejected

Status: Open.

#191 In coord-e/thrust;

· coord-e opened on Jul 24, 2026

Unsound: a generic trait impl method's body is never checked against the trait method's spec, so callers assume an unverified ensures and panicking programs verify as safe

Status: Open.

#190 In coord-e/thrust;

· coord-e opened on Jul 23, 2026

Incompleteness: overriding a defaulted trait method reuses the trait method's inference template, so the default body's return value pollutes the override's inferred spec — safe programs are wrongly rejected

Status: Open.

#187 In coord-e/thrust;

· coord-e opened on Jul 22, 2026

Incompleteness: an explicit invariant! havocs live locals it doesn't mention, even when the loop never modifies them, wrongly rejecting safe programs

Status: Open.

#186 In coord-e/thrust;

· coord-e opened on Jul 21, 2026

Unsound: unsigned integer constants with the high bit set (e.g. u8 = 200) are decoded as negative in const_value_ty, so always-panicking programs verify as safe

bugSomething isn't workingSomething isn't working

Status: Open.

#180 In coord-e/thrust;

· coord-e opened on Jul 18, 2026

Unsound: a function annotated only with sig/ret/param whose body violates the declared refinement verifies as safe when it is not called (unspecified param precondition becomes an inference template that is discharged vacuously)

bugSomething isn't workingSomething isn't working

Status: Open.

#179 In coord-e/thrust;

· coord-e opened on Jul 16, 2026

Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field

bugSomething isn't workingSomething isn't working

Status: Open.

#178 In coord-e/thrust;

· coord-e opened on Jul 13, 2026

Unsound: moving a &mut-capturing closure out of a tuple/struct field into a by-value FnOnce/FnMut verifies panicking programs as safe

bugSomething isn't workingSomething isn't working

Status: Open.

#177 In coord-e/thrust;

· coord-e opened on Jul 13, 2026

Panic: "borrowing unbound var" when writing through a reassigned &mut local

bugSomething isn't workingSomething isn't working

Status: Open.

#176 In coord-e/thrust;

· coord-e opened on Jul 12, 2026

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

Status: Open.

#175 In coord-e/thrust;

· coord-e opened on Jul 10, 2026