More relevant information on hovering failing assertions

[MikaelMayer]

Dafny version

3.10.0

Code to produce this issue

predicate P(i: int) {
  i <= 0
}

predicate Q(i: int, j: int) {
  i == j || -i == j
}

function method Toast(i: int): int
  requires P(i)

method Test(i: int) returns (j: nat)
  ensures Q(i, j)
{
  if i < 0 {
    return -i;
  } else {
    return Toast(i);
  }
}

Command to run and resulting output

Paste this code in VSCode.

If you hover over Q(i, j) (the failing postcondition), it does not tell you exactly which of the conjuncts of Q is failing
If you hover over the last "return" keyword, it just tell you that a postcondition is failing, but not which one.
If you hover over the call to Toast, it tells you that a function precondition might not hold, but it does not tell you which one.

What happened?

Currently, when we hover in the IDE an error message, we don't get all the related locations nor the related code.
Even worse, when we introduce a resolution error, hovering over it hides it under a potential ton of obsolete verification error. They should be removed from hovering.
All of this is extremely frustrating for a advanced Dafny developer like me, when using nested predicates, etc.
It could be marked as a "feature" but it's so frustrating that it was not taken account in the original design that I mark it as an error reporting bug.

What type of operating system are you experiencing the problem on?

Windows