A precondition for this call might not hold ... return path?

[MikaelMayer]

I found this strange warning for the following code, when hovering the call Test2(0)

method Test1() {
    Test2(0);
}

method Test2(i: int)
  requires i > 0 {

}

It should have say "required precondition" instead of "return path".
And even better, it should actually state the required precondition rather than pointing to it.