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

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

Yiping106283 wants to merge 2 commits into

EasyCrypt:mainEasyCrypt/easycrypt:mainfrom

Yiping106283:fix-phoare-while-variant-entryYiping106283/easycrypt:fix-phoare-while-variant-entryCopy head branch name to clipboard