We were using Boogie (via Rise4Fun) in an exercise class this afternoon, and some students found that they were able to "verify" variants of the following minimal example (key ingredients: a negative number followed by a while loop):
I'm guessing that the version of Boogie on R4F is old, and that updating it will resolve the issue, since the latest (offline) version of Boogie correctly reports the postcondition violation.
Might it be possible to look into this (or at least point me to who to contact regarding R4F)?
with best wishes,
-- Chris P.