Ignored or could not reach conclusion not highlighted in gutter

[MikaelMayer]

Dafny version

4.0.0

Code to produce this issue

No response

Command to run and resulting output

function fib(n: nat): nat {
  if n <= 1 then n else fib(n-1) + fib(n-2)
}

method {:rlimit 1} Test(s: seq<nat>)
  requires |s| >= 1 && s[0] >= 0 {
  assert fib(10) == 1; assert {:split_here} s[0] >= 0;
}

What happened?

Püt this code in VSCode. You'll get:

Notably, an error context without error, but also a check on the line where the "could not reach conclusion" assertion is located.

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

Windows