Diverging modifies clauses cause unsound vacuity #2909
Description
Diverging (panicking) expressions, such as indexing, in a modifies clause lead to vacuous verification.
{{ message }}
modifies clauses cause unsound vacuity #2909Diverging (panicking) expressions, such as indexing, in a modifies clause lead to vacuous verification.