Errflag1

var p : bool
var q : bool

export action act = {
    p := true;
    while q
    invariant p
    invariant p
    invariant p
    invariant p
    invariant p
    invariant p
    invariant p
    invariant p
    {
        assert p;
        p := p;
        q := *
    };
    assert ~q
}