Search results

Unsound: enum variants after an explicit discriminant get the wrong datatype_discr value, making match arms vacuously verify

bugSomething isn't workingSomething isn't working

Status: Open.

#126 In coord-e/thrust;

· coord-e opened on Jun 13, 2026

Panic: "deref unbound var" when reborrowing a &mut field out of an aggregate parameter

bugSomething isn't workingSomething isn't working

Status: Open.

#125 In coord-e/thrust;

· coord-e opened on Jun 13, 2026

Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy

bugSomething isn't workingSomething isn't working

Status: Open.

#122 In coord-e/thrust;

· coord-e opened on Jun 13, 2026

Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows

bugSomething isn't workingSomething isn't working

Status: Open.

#121 In coord-e/thrust;

· coord-e opened on Jun 12, 2026

Panic in const_value_ty when analyzing integer constants larger than i64::MAX

bugSomething isn't workingSomething isn't working

Status: Open.

#116 In coord-e/thrust;

· coord-e opened on Jun 9, 2026

Panics in solver.rs: unwrap on env-var parse and on timeout when no timeout is set

bugSomething isn't workingSomething isn't working

Status: Open.

#113 In coord-e/thrust;

· coord-e opened on Jun 8, 2026

Unsigned integer constants sign-extended incorrectly in const_value_ty, causing wrong CHC terms and potential panic

bugSomething isn't workingSomething isn't working

Status: Open.

#110 In coord-e/thrust;

· coord-e opened on Jun 7, 2026

Support logical implication syntax in annotations

Status: Open.

#106 In coord-e/thrust;

· coord-e opened on Jun 6, 2026

Refinements on Box (own-pointer) pointee in return position are not enforced — unsound

bugSomething isn't workingSomething isn't working

Status: Open.

#97 In coord-e/thrust;

· coord-e opened on May 26, 2026

Refer to pre-/post-conditions of other defs in specifications

Status: Open.

#83 In coord-e/thrust;

· coord-e opened on May 10, 2026

Drop old annotation parser implementation

Status: Open.

#70 In coord-e/thrust;

· coord-e opened on May 1, 2026

Enable to specify backend CHC solver via attributes

Status: Open.

#69 In coord-e/thrust;

· coord-e opened on Apr 30, 2026