Search results

Integer division (/) and remainder (%) abort with unimplemented!, and bypass div-by-zero / MIN / -1 panic checking

bugSomething isn't workingSomething isn't working

Status: Open.

#144 In coord-e/thrust;

· coord-e opened on Jun 22, 2026

Quantifier (forall/exists) binder sorts are never declared in SMT-LIB, so any spec quantifying over a datatype/tuple-sorted variable emits an undefined sort

bugSomething isn't workingSomething isn't working

Status: Open.

#142 In coord-e/thrust;

· coord-e opened on Jun 18, 2026

Panic unimplemented!(unrefined_ty: FnDef(..)) when passing a named function (function item) to a higher-order function

bugSomething isn't workingSomething isn't working

Status: Open.

#140 In coord-e/thrust;

· coord-e opened on Jun 18, 2026

Boolean comparisons (<, <=, >, >=) emit ill-typed SMT (< Bool Bool), so any program comparing bools fails to verify

Status: Open.

#136 In coord-e/thrust;

· coord-e opened on Jun 16, 2026

Unsound: negative SwitchInt match targets are sign-truncated to large positives, making match arms verify under a wrong path assumption

bugSomething isn't workingSomething isn't working

Status: Open.

#132 In coord-e/thrust;

· coord-e opened on Jun 15, 2026

Incompleteness: function-type subtyping in relate_sub_type proves the return obligation without assuming the parameters' preconditions

bugSomething isn't workingSomething isn't working

Status: Open.

#128 In coord-e/thrust;

· coord-e opened on Jun 14, 2026

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