Skip to content

fix(phl): require the invariant on loop entry in the while variant rule - #1132

Merged
oskgo merged 1 commit into
EasyCrypt:mainfrom
Yiping106283:fix-phoare-while-variant-entry
Oct 30, 2026
Merged

fix(phl): require the invariant on loop entry in the while variant rule#1132
oskgo merged 1 commit into
EasyCrypt:mainfrom
Yiping106283:fix-phoare-while-variant-entry

fix(phl): require the invariant on loop entry in the `while` variant …

2f922c6
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
Decide whether to run the CI
succeeded Oct 30, 2026 in 4s