weird error message: "(0,-1): Error: a postcondition"

[kjx]

Failing code

too much to paste (down to 6K lines)

(0,-1): Error: a postcondition could not be proved on this return path

Steps to reproduce the issue

• Dafny version: 4.7.0.0
• Dafny VSCode extension version: 3.3.1

Expected behavior

(line number, column number)

Actual behavior

(0,-1)

[keyboardDrummer]

If you figure out which piece of code the error is about, please add it to this issue.

[kjx]

If I can isolate the code I will, otherwise it's not a super-high priority (although you could put a trap in for an error report on line 0 or column -1) James

…

On 15 Aug 2024, at 21:36, Remy Willems ***@***.***> wrote: If you figure out which piece of code the error is about, please add it to this issue.

[kjx]

Dunno if this helps but theIDE just gave me this popup also with a zero line number.