Verification symbols not correct when a declaration is marked {:only}

[MikaelMayer]

Dafny version

4.2.0

Code to produce this issue

method NotVerified() { // Should not be highlighted in green
  assert 1 == 0;
}
method {:only} Verified() { // Verified
  assert true;
}
method NotVerified2() { // Should not be highlighted in green
  assert 1 == 0;
}

Command to run and resulting output

Paste in VSCode with "Verification as tests" turned on, and gutter icons turned off.

What happened?

It's an issue similar to #4432 although verification symbols are a different API so it requires a different fix.

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

Windows

[keyboardDrummer]

I plan to make play icons appear in front of assertions when --isolate-assertions or {:isolate_assertions} is used, at which point I think the IDE play icons and --filter-position option fill a similar role as {:only}. @MikaelMayer how do you feel about having these similar features? {:only} also has variations with before and after, and I could imagine a similar feature in --filter-position, where you space a line range instead of a single line.

[MikaelMayer]

It sounds like these icons would integrate nicely with {:only}

[keyboardDrummer]

It sounds like these icons would integrate nicely with {:only}

How do you mean? I would think they solve a similar problem as {:only}, but in the IDE only, just like --filter-position solves a similar problem as {:only}, but only on the CLI.

[MikaelMayer]

I mean that if you put {:only} on one assertion, you would only see the green or red icons next to the assertion to verify.
But the purpose of {:only} is when verification is on change. Would you have a way in your icons so that verification on change would be constrained?

[keyboardDrummer]

Would you have a way in your icons so that verification on change would be constrained?

No, the play icons are purely output when you're using verification on change.

I guess when we have assertion level verification caching, you will be able to use verification on change and not need to use either the play icons or {:only}.

[MikaelMayer]

I guess when we have assertion level verification caching, you will be able to use verification on change and not need to use either the play icons or {:only}.

Oh yeah, that would be fantastic.