Flaky test: git-issue-3855.dfy about dafny HOT 7 CLOSED

Here is my preferred fix: #5393

from dafny.

Actually looks like a legit regression since it failed on retry as well: https://github.com/dafny-lang/dafny/actions/runs/8910687756/job/24474173302#step:22:412

from dafny.

It passed on the third try. The problem was that a timeout was expected after 1 second, but occurred after 6 seconds. This is the only test that has the timeout hardcoded in this way. The relevant function has its timelimit set to 1 second, so it is unclear to me why it can fail after 6 seconds. I'll close the issue as the immediate problem is resolved and suggest we reopen and perhaps ignore that function if this particular test throws an error again.

from dafny.

Thanks for unblocking the nightly build @stefan-aws. Reopening this as we want to track flaky tests in general and drive them down, though. This one seems very likely to recur to me given it failed on 2 out of 3 attempts.

from dafny.

Looks like a bug in the implementation, not in the tests.

from dafny.

Possibly a race condition in the multiple mechanisms for timing out in the pipeline?

I removed one of them so I think it's only Boogie handling the timeout now.

from dafny.

I think I changed the time out reporting so that it reports the actual amount of seconds the run took, instead of the configured time, and that makes this test unstable. Note that the current code has a bug anyways because it calls TimeSpan.Seconds instead of TimeSpan.TotalSeconds.

Here's a PR that lets it report the configured time out instead of the actual time taken: #5392

Alternatively, we can change the test so it redacts the line on which it is currently failing, so it won't be unstable

from dafny.