Hello,

I just ran into a problem. I can not actually find the rules for `pc`

for a while loop and applying the one I have written down yields something wrong. The while rule for `vc`

is on page 12 of the speficiation, this is my rule for `pc`

:

```
pc while(e)_Invariant(i)_Term(t; k) Q = i && (0 <= t <= k + 1)
```

I think the problem might be that I added the termination condition at all.

For example I test this program and get an assertion error:

```
int x;
_Assume(x >= 0);
while(x != 0)_Inv(1)_Term(x; k) {
x = x - 1;
}
_Assert(x == 0);
```

I computed `vc`

and `pc`

by hand and using the above formula I get:

```
pc ... true = (x >= 0) => (0 <= x <= k + 1)
// this is equivalent to:
(x >= 0) => (x <= k + 1)
vc ... true = true
```

If in the formula for `pc`

I only return the invariant I would get that `pc ... true = true`

.