You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
As part of the epic on verification stability (dafny-lang/dafny#1582), I've found that the implementation of the {:split_here} and {:focus} directives can easily be reused to isolate every assertion in its own split, just as if {:split_here} was present on every assertion. I have a POC implementation that has proven useful as a debugging tool, to identify which asserts in a procedure were by far the most expensive to verify. Focusing on improving those assertions then greatly improved the stability of the procedure.
The equivalent {:vcs_split_on_every_assert} attribute would also be useful as a blunt instrument for improving the stability of a procedure: although it would increase the total verification time quite a bit because of the overhead, it would also greatly improve the stability of the verification.
The text was updated successfully, but these errors were encountered:
As part of the epic on verification stability (dafny-lang/dafny#1582), I've found that the implementation of the
{:split_here}
and{:focus}
directives can easily be reused to isolate every assertion in its own split, just as if{:split_here}
was present on every assertion. I have a POC implementation that has proven useful as a debugging tool, to identify which asserts in a procedure were by far the most expensive to verify. Focusing on improving those assertions then greatly improved the stability of the procedure.The equivalent
{:vcs_split_on_every_assert}
attribute would also be useful as a blunt instrument for improving the stability of a procedure: although it would increase the total verification time quite a bit because of the overhead, it would also greatly improve the stability of the verification.The text was updated successfully, but these errors were encountered: