MRE: ``` require import Real. module M = {proc p() = {while (true) {}}}. lemma bad: phoare[M.p: true ==> false] <= (-1%r). proof. proc. while (true). auto. done. qed. ```
Activity
fix(phl): check the bound of the upper-bound `while` rule on all memo…
fix(phl): reject a bound written by the prefix in the upper-bound `wh…
fix(phl): check the bound of the upper-bound `while` rule on all memo…
fix(phl): check the bound of the upper-bound `while` rule on all memo…
fix(phl): check the bound of the upper-bound `while` rule on all memo…
fix(phl): check the bound of the upper-bound `while` rule on all memo…
fix(phl): reject a bound written by the prefix in the upper-bound `wh…
fix(phl): check the bound of the upper-bound `while` rule on all memo…