Introduce an {:isolate_branches}
attribute that can be used at the method level
#5817
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
priority: not yet
Will reconsider working on this when we're looking for work
{:isolate_branches}
would provide a weaker form of{:isolate_assertions}
, by only creating a separate VC for each branch in the method. This way, different branches of the same conditional construct would be isolated. Not doing so can lead to rather surprising verification behavior, where changes in one branch effecting the verification of a sibling branch.We could consider making
{:isolate_branches}
the default, since it is relatively cheap compared to{:isolate_assertions}
.The text was updated successfully, but these errors were encountered: