Simple verification example case with permissions. A shared variable `val` is updated in a loop, but the order of the clauses in the loop invariant do matter here. This example is failing, since the `Perm(val,100)` invariant clause needs to be placed before the `val+tmp==\old(val)+n && tmp>0` clause.
Path to example file
Lines of code
16 lines (comments not included)
Lines of specification
4 lines (25% of the total)
Note, verification may take a while and has a time-out of 20 seconds.