Perhaps the most fundamental definition of verification instability is that the outcome of verification differs between verification attempts. The CSV input consumed by dafny-reportgenerator includes an Outcome field, and this PR now causes the summarize-csv-results command to fail if the number of distinct outcome types for a given procedure is greater than 1. Given that this is always an indication of instability, this check is unconditional.
Perhaps the most fundamental definition of verification instability is that the outcome of verification differs between verification attempts. The CSV input consumed by
dafny-reportgeneratorincludes anOutcomefield, and this PR now causes thesummarize-csv-resultscommand to fail if the number of distinct outcome types for a given procedure is greater than 1. Given that this is always an indication of instability, this check is unconditional.