IDE crash when verifying method

[rod-chapman]

Verifying some code with Dafny 3.9.1 and VSCode Extension 2.8.6.

I get:

Unhandled exception. System.ArgumentException: An item with the same key has already been added. Key: assert LitInt(0) <= newtype$check#36#AT#0 && newtype$check#36#AT#0 < BoundedInts.__default.TWO__TO__THE__32();

at System.Collections.Generic.Dictionary2.TryInsert(TKey key, TValue value, InsertionBehavior behavior) at VC.VCResult.ComputePerAssertOutcomes(Dictionary2& perAssertOutcome, Dictionary2& perAssertCounterExamples) at Microsoft.Dafny.LanguageServer.Workspace.VerificationProgressReporter.ReportAssertionBatchResult(AssertionBatchResult batchResult) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/out/resources/3.9.1/custom/arm64/dafny/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs:line 298 at System.Reactive.AnonymousSafeObserver1.OnNext(T value) in //Rx.NET/Source/src/System.Reactive/AnonymousSafeObserver.cs:line 54
at System.Reactive.ObserveOnObserverNew1.DrainStep(ConcurrentQueue1 q) in //Rx.NET/Source/src/System.Reactive/Internal/ScheduledObserver.cs:line 559
at System.Reactive.ObserveOnObserverNew`1.DrainShortRunning(IScheduler recursiveScheduler) in //Rx.NET/Source/src/System.Reactive/Internal/ScheduledObserver.cs:line 513
at System.Reactive.Concurrency.EventLoopScheduler.Run() in //Rx.NET/Source/src/System.Reactive/Concurrency/EventLoopScheduler.cs:line 356
at System.Threading.Thread.StartHelper.Callback(Object state)
at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
at System.Runtime.ExceptionServices.ExceptionDispatchInfo.Throw()
[Info - 4:13:23 PM] Connection to server got closed. Server will restart.
[Error - 4:13:23 PM] Request textDocument/codeAction failed.
Error: Connection got disposed.
at Object.dispose (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:273538)
at Object.dispose (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:353621)
at u.handleConnectionClosed (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:353834)
at u.handleConnectionClosed (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:414180)
at t (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:351923)
at a.invoke (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:275151)
at n.fire (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:275912)
at Z (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:262796)
at a.invoke (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:275151)
at n.fire (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:275912)
at g.fireClose (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:287365)
at Socket. (/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.6/dist/extension.js:1:288150)
at Socket.emit (node:events:526:28)
at Pipe. (node:net:687:12)

[rod-chapman]

Thanks for fixing this. Please let me know when a new release is available that incorporates this.

[MikaelMayer]

The latest Dafny nightly fixes this issue