When Dafny verification runs out of time or tick resources, automatically rerun verification with {:isolate_assertions}
#5819
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
misc: brittleness
When Dafny sometimes proves something, and sometimes doesn't
part: verifier
Translation from Dafny to Boogie (translator)
When Dafny verification runs out of time or tick resources, automatically rerun verification with
{:isolate_assertions}
to pinpoint the problematic assertions, and advise adding{:isolate}
to these to help improve and debug performance.The text was updated successfully, but these errors were encountered: