Remy Willems

With the above I can reproduce it. Note that just `--type-system-refresh` is not enough

> To improve on this, we could run the tests only once in the step, but allow that step to be retried a few times (maybe 3) if it fails....

There should be a log line in the test log that comes from this line of code: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs#L61 But it's not there. Based on the stack trace I don't see...

Problem was that `notifications.Dequeue(cancellationToken)` is not awaited within the `try/catch`

PR to help debug this issue the next time it occurs: https://github.com/dafny-lang/dafny/pull/5386

For anyone who runs into this after the above PR is merged, please add your log link to this issue

> > Lots of things > > LOL > Fixed 😅 > Is making verification consistent in scope? Was not but is now :)

This has mostly been resolved by https://github.com/dafny-lang/dafny/pull/4798 and https://github.com/dafny-lang/dafny/pull/5008 I wonder what we can further do to guarantee same generated SMT between server and CLI

I agree, this is unexpected behavior.

Relevant boogie code for the above program: ``` // function declaration for _module._default.Hidden2 function _module.__default.Hidden2($reveal: bool) : int uses { // consequence axiom for _module.__default.Hidden2 axiom 1 (forall $reveal: bool...