Bound not recognized right after refining a spec with a loop

Load the file:
```
con A, B : Int 
var r, a, b : Int

{ r + a * b = A * B, bnd: b }
[!
do b ≠ 0 -> skip
od
!]
{ r = A * B }
```
and refine the spec. We get a warning
```
Warning at 5:1-6:3#MissingBound
A bound is required to prove the termination of the loop.
```
even though there is a bound `bnd: b`. Loading (`ctrl-c-l`) the file again and things get normal.