diff --git a/Source/DafnyCore.Test/NodeTests.cs b/Source/DafnyCore.Test/NodeTests.cs
index e4a52d860f1..3e376b0b253 100644
--- a/Source/DafnyCore.Test/NodeTests.cs
+++ b/Source/DafnyCore.Test/NodeTests.cs
@@ -1,7 +1,7 @@
 using System.Collections.Concurrent;
 using Microsoft.Dafny;
 
-namespace DafnyCore.Test; 
+namespace DafnyCore.Test;
 
 public class NodeTests {
 
diff --git a/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs b/Source/DafnyCore.Test/WriterFromOutputHelper.cs
similarity index 66%
rename from Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs
rename to Source/DafnyCore.Test/WriterFromOutputHelper.cs
index 8448d66eb33..dcc5aed0027 100644
--- a/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs
+++ b/Source/DafnyCore.Test/WriterFromOutputHelper.cs
@@ -1,13 +1,8 @@
-// Copyright by the contributors to the Dafny Project
-// SPDX-License-Identifier: MIT
-
-#nullable disable
-using System.IO;
+#nullable enable
 using System.Text;
-using Microsoft.Extensions.Primitives;
 using Xunit.Abstractions;
 
-namespace DafnyTestGeneration.Test;
+namespace DafnyCore.Test;
 
 public class WriterFromOutputHelper : TextWriter {
   private readonly StringBuilder buffer = new();
@@ -17,7 +12,7 @@ public WriterFromOutputHelper(ITestOutputHelper output) {
     this.output = output;
   }
 
-  public override void Write(string value) {
+  public override void Write(string? value) {
     if (value != null) {
       buffer.Append(value);
     }
@@ -29,12 +24,12 @@ public override void Write(char value) {
 
   public override Encoding Encoding => Encoding.Default;
 
-  public override void WriteLine(string value) {
+  public override void WriteLine(string? value) {
     output.WriteLine(buffer + value);
     buffer.Clear();
   }
 
-  public override void WriteLine(string format, params object[] arg) {
+  public override void WriteLine(string format, params object?[] arg) {
     output.WriteLine(buffer + format, arg);
     buffer.Clear();
   }
diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs
index 47800c4ae4d..af67b09e0f5 100644
--- a/Source/DafnyCore/DafnyFile.cs
+++ b/Source/DafnyCore/DafnyFile.cs
@@ -1,7 +1,6 @@
 using System;
 using System.Collections.Generic;
 using System.IO;
-using System.Linq;
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
 using DafnyCore;
diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs
index f1ad8784bc3..8576c45e229 100644
--- a/Source/DafnyCore/Options/DafnyProject.cs
+++ b/Source/DafnyCore/Options/DafnyProject.cs
@@ -56,37 +56,67 @@ public IEnumerable<Uri> GetRootSourceUris(IFileSystem fileSystem) {
     if (!Uri.IsFile) {
       return new[] { Uri };
     }
+    var matcher = GetMatcher(out var searchRoot);
 
-    var matcher = GetMatcher();
-
-    var diskRoot = Path.GetPathRoot(Uri.LocalPath);
-    var result = matcher.Execute(fileSystem.GetDirectoryInfoBase(diskRoot));
-    var files = result.Files.Select(f => Path.Combine(diskRoot, f.Path));
+    var result = matcher.Execute(fileSystem.GetDirectoryInfoBase(searchRoot));
+    var files = result.Files.Select(f => Path.Combine(searchRoot, f.Path));
     return files.Select(file => new Uri(Path.GetFullPath(file)));
   }
 
   public bool ContainsSourceFile(Uri uri) {
-    var fileSystemWithSourceFile = new InMemoryDirectoryInfoFromDotNet8(Path.GetPathRoot(uri.LocalPath)!, new[] { uri.LocalPath });
-    return GetMatcher().Execute(fileSystemWithSourceFile).HasMatches;
+    var matcher = GetMatcher(out var searchRoot);
+    var fileSystemWithSourceFile = new InMemoryDirectoryInfoFromDotNet8(searchRoot, new[] { uri.LocalPath });
+    return matcher.Execute(fileSystemWithSourceFile).HasMatches;
   }
 
-  private Matcher GetMatcher() {
+  private Matcher GetMatcher(out string commonRoot) {
     var projectRoot = Path.GetDirectoryName(Uri.LocalPath)!;
-    var root = Path.GetPathRoot(Uri.LocalPath)!;
+    var diskRoot = Path.GetPathRoot(Uri.LocalPath)!;
+
+    var includes = Includes ?? new[] { "**/*.dfy" };
+    var excludes = Excludes ?? Array.Empty<string>();
+    var fullPaths = includes.Concat(excludes).Select(p => Path.GetFullPath(p, projectRoot)).ToList();
+    commonRoot = GetCommonParentDirectory(fullPaths) ?? diskRoot;
     var matcher = new Matcher();
-    foreach (var includeGlob in Includes ?? new[] { "**/*.dfy" }) {
-      var fullPath = Path.GetFullPath(includeGlob, projectRoot);
-      matcher.AddInclude(Path.GetRelativePath(root, fullPath));
+    foreach (var includeGlob in includes) {
+      matcher.AddInclude(Path.GetRelativePath(commonRoot, Path.GetFullPath(includeGlob, projectRoot)));
     }
 
-    foreach (var includeGlob in Excludes ?? Enumerable.Empty<string>()) {
-      var fullPath = Path.GetFullPath(includeGlob, projectRoot);
-      matcher.AddExclude(Path.GetRelativePath(root, fullPath));
+    foreach (var excludeGlob in excludes) {
+      matcher.AddExclude(Path.GetRelativePath(commonRoot, Path.GetFullPath(excludeGlob, projectRoot)));
     }
 
     return matcher;
   }
 
+  string GetCommonParentDirectory(IReadOnlyList<string> strings) {
+    if (!strings.Any()) {
+      return null;
+    }
+    var commonPrefix = strings.FirstOrDefault() ?? "";
+
+    foreach (var newString in strings) {
+      var potentialMatchLength = Math.Min(newString.Length, commonPrefix.Length);
+
+      if (potentialMatchLength < commonPrefix.Length) {
+        commonPrefix = commonPrefix.Substring(0, potentialMatchLength);
+      }
+
+      for (var i = 0; i < potentialMatchLength; i++) {
+        if (newString[i] == '*' || newString[i] != commonPrefix[i]) {
+          commonPrefix = commonPrefix.Substring(0, i);
+          break;
+        }
+      }
+    }
+
+    if (!Path.EndsInDirectorySeparator(commonPrefix)) {
+      commonPrefix = Path.GetDirectoryName(commonPrefix);
+    }
+
+    return commonPrefix;
+  }
+
   public void Validate(TextWriter outputWriter, IEnumerable<Option> possibleOptions) {
     if (Options == null) {
       return;
diff --git a/Source/DafnyDriver/DafnyDoc.cs b/Source/DafnyDriver/DafnyDoc.cs
index 443b9272e9b..2632b14102f 100644
--- a/Source/DafnyDriver/DafnyDoc.cs
+++ b/Source/DafnyDriver/DafnyDoc.cs
@@ -50,8 +50,6 @@ public static DafnyDriver.ExitValue DoDocumenting(IReadOnlyList<DafnyFile> dafny
       outputdir = DefaultOutputDir;
     }
 
-
-
     // Collect all the dafny files; dafnyFiles already includes files from a .toml project file
     var exitValue = DafnyDriver.ExitValue.SUCCESS;
     dafnyFiles = dafnyFiles.Concat(dafnyFolders.SelectMany(folderPath => {
diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj
index 392fa360a6c..a21d680f516 100644
--- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj
+++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj
@@ -10,7 +10,7 @@
     <PackageReference Include="DiffPlex" Version="1.7.0" />
     <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="3.7.0" />
     <PackageReference Include="Microsoft.Extensions.Logging.Console" Version="5.0.0" />
-    <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.11.0" />
+    <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.1.0" />
     <PackageReference Include="Moq" Version="4.16.1" />
     <PackageReference Include="Serilog.Sinks.InMemory" Version="0.11.0" />
     <PackageReference Include="xunit" Version="2.4.2" />
@@ -25,6 +25,7 @@
   </ItemGroup>
 
   <ItemGroup>
+    <ProjectReference Include="..\DafnyCore.Test\DafnyCore.Test.csproj" />
     <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
   </ItemGroup>
 
diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
index e75822dca20..674cc84af66 100644
--- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
+++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
@@ -16,6 +16,7 @@
 using System.Linq;
 using System.Threading;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Various;
 using Microsoft.Dafny.LanguageServer.Language;
 using OmniSharp.Extensions.LanguageServer.Client;
@@ -94,6 +95,7 @@ public AnonymousDisposable(Action action) {
 
     private Action<LanguageServerOptions> GetServerOptionsAction(Action<DafnyOptions> modifyOptions) {
       var dafnyOptions = DafnyOptions.Create(output);
+      dafnyOptions.Set(ServerCommand.UpdateThrottling, 0);
       modifyOptions?.Invoke(dafnyOptions);
       ServerCommand.ConfigureDafnyOptionsForServer(dafnyOptions);
       ApplyDefaultOptionValues(dafnyOptions);
diff --git a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs
new file mode 100644
index 00000000000..f86ec852db6
--- /dev/null
+++ b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs
@@ -0,0 +1,111 @@
+using System;
+using System.Text;
+using System.Threading;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Xunit;
+using Xunit.Abstractions;
+using Xunit.Sdk;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Performance;
+
+public class LargeFilesTest : ClientBasedLanguageServerTest {
+  protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
+    return base.SetUp(options => {
+      modifyOptions?.Invoke(options);
+      options.Set(ServerCommand.UpdateThrottling, ServerCommand.DefaultThrottleTime);
+    });
+  }
+
+  /// <summary>
+  /// This test should complete in less than a second, because it opens a moderately sized file
+  /// on which it makes edits so quickly that the edits should all be processed in a single compilation.
+  /// And a single compilation should complete in less than 200ms.
+  ///
+  /// Right now the test still takes more than 5 seconds.
+  /// To reduce runtime of this test,
+  /// remove ReportRealtimeDiagnostics (since it is called 10 times for each update,
+  /// and calls InitialIdeState, which often calls CompilationAfterResolution.ToIdeState (expensive))
+  /// </summary>
+  [Fact]
+  public async Task QuickEditsInLargeFile() {
+    string GetLineContent(int index) => $"method Foo{index}() {{ assume false; }}";
+    var contentBuilder = new StringBuilder();
+    for (int lineNumber = 0; lineNumber < 1000; lineNumber++) {
+      contentBuilder.AppendLine(GetLineContent(lineNumber));
+    }
+    var source = contentBuilder.ToString();
+
+    double lowest = double.MaxValue;
+    Exception lastException = null;
+    try {
+      for (int attempt = 0; attempt < 10; attempt++) {
+        var cancelSource = new CancellationTokenSource();
+        var measurementTask = AssertThreadPoolIsAvailable(cancelSource.Token);
+        var beforeOpen = DateTime.Now;
+        var documentItem = await CreateAndOpenTestDocument(source, "ManyFastEditsUsingLargeFiles.dfy",
+          cancellationToken: CancellationTokenWithHighTimeout);
+        var afterOpen = DateTime.Now;
+        var openMilliseconds = (afterOpen - beforeOpen).TotalMilliseconds;
+        for (int i = 0; i < 100; i++) {
+          ApplyChange(ref documentItem, new Range(0, 0, 0, 0), "// added this comment\n");
+        }
+
+        await client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationTokenWithHighTimeout);
+        var afterChange = DateTime.Now;
+        var changeMilliseconds = (afterChange - afterOpen).TotalMilliseconds;
+        await AssertNoDiagnosticsAreComing(CancellationTokenWithHighTimeout);
+        cancelSource.Cancel();
+        var averageTimeToSchedule = await measurementTask;
+        var division = changeMilliseconds / openMilliseconds;
+        lowest = Math.Min(lowest, division);
+
+        // Commented code left in intentionally
+        // await output.WriteLineAsync("openMilliseconds: " + openMilliseconds);
+        // await output.WriteLineAsync("changeMilliseconds: " + changeMilliseconds);
+        // await output.WriteLineAsync("division: " + division);
+        try {
+          Assert.True(averageTimeToSchedule < 100);
+          // Migration should be constant time, which would allow this number to be about 1.
+          // Right now migration is still slow so this has been set to 10 so the test can pass.
+          var changeTimeMultiplier = 15;
+          Assert.True(division < changeTimeMultiplier,
+            $"changeMilliseconds {changeMilliseconds}, openMilliseconds {openMilliseconds}");
+
+          return;
+        } catch (AssertActualExpectedException e) {
+          lastException = e;
+        }
+      }
+    } catch (OperationCanceledException) {
+    }
+
+    await output.WriteLineAsync("lowest division " + lowest);
+    throw lastException!;
+  }
+
+  private async Task<double> AssertThreadPoolIsAvailable(CancellationToken durationToken) {
+    int ticks = 0;
+    var waitTime = 100;
+    var start = DateTime.Now;
+    while (!durationToken.IsCancellationRequested) {
+      await Task.Run(() => {
+        Thread.Sleep(waitTime);
+      });
+      ticks++;
+    }
+
+    var end = DateTime.Now;
+    var span = end - start;
+    var totalSleepTime = ticks * waitTime;
+    var totalSchedulingTime = span.TotalMilliseconds - totalSleepTime;
+    var averageTimeToSchedule = totalSchedulingTime / ticks;
+    // await output.WriteLineAsync($"averageTimeToSchedule: {averageTimeToSchedule:0.##}");
+    return averageTimeToSchedule;
+  }
+
+  public LargeFilesTest(ITestOutputHelper output) : base(output) {
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
index 5a57a327cec..0da11b10df7 100644
--- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
+++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
@@ -99,23 +99,30 @@ method Foo() {
   }
 
   [Fact]
-  public async Task FileOnlyAttachedToProjectFileThatAppliesToIt() {
+  public async Task FileOnlyAttachedToProjectFileThatIncludesIt() {
     await SetUp(options => options.WarnShadowing = false);
 
-    var projectFileSource = @"
+    var outerSource = @"
 [options]
 warn-shadowing = true
 ";
     var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
-    var outerProjectFile = CreateTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName));
+    var outerProjectFile = CreateTestDocument(outerSource, Path.Combine(directory, DafnyProject.FileName));
     await client.OpenDocumentAndWaitAsync(outerProjectFile, CancellationToken);
 
-    var innerProjectFile = CreateTestDocument("includes = []", Path.Combine(directory, "nested", DafnyProject.FileName));
+    var innerDirectory = Path.Combine(directory, "nested");
+    var innerProjectFile = CreateTestDocument("includes = []", Path.Combine(innerDirectory, DafnyProject.FileName));
     await client.OpenDocumentAndWaitAsync(innerProjectFile, CancellationToken);
 
-    var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/noWarnShadowing.dfy");
-    var source = await File.ReadAllTextAsync(filePath);
-    var documentItem = CreateTestDocument(source, Path.Combine(directory, "nested/A.dfy"));
+    var source = @"
+method Foo() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}
+";
+    var documentItem = CreateTestDocument(source, Path.Combine(innerDirectory, "A.dfy"));
     await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
     var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
     Assert.Single(diagnostics);
diff --git a/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs b/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs
index f5c8f9b8021..7d7bbdc0f14 100644
--- a/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs
+++ b/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs
@@ -1,6 +1,7 @@
 using System;
 using System.IO;
 using System.Text;
+using DafnyCore.Test;
 using Microsoft.Dafny.LanguageServer.Workspace;
 using Xunit.Abstractions;
 using Xunit;
@@ -21,29 +22,3 @@ public void OptionParsing() {
     Assert.Equal(VerifyOnMode.Save, options.Get(ServerCommand.Verification));
   }
 }
-
-public class WriterFromOutputHelper : TextWriter {
-  private readonly ITestOutputHelper output;
-  private bool failed = false;
-
-  public WriterFromOutputHelper(ITestOutputHelper output) {
-    this.output = output;
-  }
-
-  public override void Write(char value) {
-    if (!failed) {
-      failed = true;
-      WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support.");
-    }
-  }
-
-  public override Encoding Encoding => Encoding.Default;
-
-  public override void WriteLine(string value) {
-    output.WriteLine(value);
-  }
-
-  public override void WriteLine(string format, params object[] arg) {
-    output.WriteLine(format, arg);
-  }
-}
diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs
index 26d41264810..1e127fe5326 100644
--- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs
+++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs
@@ -924,16 +924,17 @@ method test() {
 ".TrimStart();
       var documentItem = CreateTestDocument(source, "IncrementalVerificationDiagnosticsBetweenMethods.dfy");
       client.OpenDocument(documentItem);
-      var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
+      var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken);
       try {
         var secondVerificationDiagnostics =
           await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
 
-        Assert.Single(firstVerificationDiagnostics);
+        Assert.Single(firstVerificationDiagnostics.Diagnostics);
         // Second diagnostic is a timeout exception from SlowToVerify
         Assert.Equal(2, secondVerificationDiagnostics.Length);
       } catch (OperationCanceledException) {
         await output.WriteLineAsync($"firstVerificationDiagnostics: {firstVerificationDiagnostics.Stringify()}");
+        WriteVerificationHistory();
       }
       await AssertNoDiagnosticsAreComing(CancellationToken);
     }
diff --git a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs
index 92ca320393f..b8f3441f1f2 100644
--- a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs
+++ b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs
@@ -4,6 +4,7 @@
 using System.IO;
 using System.Linq;
 using System.Threading;
+using DafnyCore.Test;
 using IntervalTree;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
@@ -32,7 +33,7 @@ public IDisposable BeginScope<TState>(TState state) {
   }
 
   public GhostStateDiagnosticCollectorTest(ITestOutputHelper output) {
-    var options = new DafnyOptions(TextReader.Null, new WriterFromOutputHelper(output), new WriterFromOutputHelper(output));
+    var options = new DafnyOptions(TextReader.Null, (TextWriter)new WriterFromOutputHelper(output), (TextWriter)new WriterFromOutputHelper(output));
     options.Set(ServerCommand.GhostIndicators, true);
     ghostStateDiagnosticCollector = new GhostStateDiagnosticCollector(
       options,
diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
index c18ccd95afa..354348a5db1 100644
--- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
+++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
@@ -8,6 +8,7 @@
 using System.IO;
 using System.Threading;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol;
@@ -67,7 +68,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
           It.IsAny<ErrorReporter>(),
           It.IsAny<CancellationToken>())).Callback(() => source.Cancel())
         .Throws<TaskCanceledException>();
-      var task = textDocumentLoader.ParseAsync(DafnyOptions.Default, GetCompilation(), ImmutableDictionary<Uri, VerificationTree>.Empty, source.Token);
+      var task = textDocumentLoader.ParseAsync(DafnyOptions.Default, GetCompilation(), ImmutableDictionary<Uri, DocumentVerificationTree>.Empty, source.Token);
       try {
         await task;
         Assert.Fail("document load was not cancelled");
@@ -90,7 +91,7 @@ public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() {
           It.IsAny<ErrorReporter>(),
           It.IsAny<CancellationToken>()))
         .Throws<InvalidOperationException>();
-      var task = textDocumentLoader.ParseAsync(DafnyOptions.Default, GetCompilation(), ImmutableDictionary<Uri, VerificationTree>.Empty, default);
+      var task = textDocumentLoader.ParseAsync(DafnyOptions.Default, GetCompilation(), ImmutableDictionary<Uri, DocumentVerificationTree>.Empty, default);
       try {
         await task;
         Assert.Fail("document load did not fail");
diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
index 13c7c976aa9..377d22b14bd 100644
--- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
+++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
@@ -47,9 +47,9 @@ protected ClientBasedLanguageServerTest(ITestOutputHelper output, LogLevel dafny
   }
 
   protected async Task<TextDocumentItem> CreateAndOpenTestDocument(string source, string filePath = null,
-    int version = 1) {
+    int version = 1, CancellationToken? cancellationToken = null) {
     var document = CreateTestDocument(source, filePath, version);
-    await client.OpenDocumentAndWaitAsync(document, CancellationToken);
+    await client.OpenDocumentAndWaitAsync(document, cancellationToken ?? CancellationToken);
     return document;
   }
 
@@ -298,7 +298,7 @@ public async Task AssertNoDiagnosticsAreComing(CancellationToken cancellationTok
       }
     }
     var verificationDocumentItem = CreateTestDocument("class X {does not parse", $"AssertNoDiagnosticsAreComing{fileIndex++}.dfy");
-    await client.OpenDocumentAndWaitAsync(verificationDocumentItem, CancellationToken);
+    await client.OpenDocumentAndWaitAsync(verificationDocumentItem, cancellationToken);
     var resolutionReport = await diagnosticsReceiver.AwaitNextNotificationAsync(cancellationToken);
     AssertM.Equal(verificationDocumentItem.Uri, resolutionReport.Uri,
       "1) Unexpected diagnostics were received whereas none were expected:\n" +
diff --git a/Source/DafnyLanguageServer.Test/Util/Stringify.cs b/Source/DafnyLanguageServer.Test/Util/Stringify.cs
index ab123ea7a96..073e65b9d40 100644
--- a/Source/DafnyLanguageServer.Test/Util/Stringify.cs
+++ b/Source/DafnyLanguageServer.Test/Util/Stringify.cs
@@ -80,6 +80,7 @@ void Helper(ImmutableHashSet<object> visited, object? value, int indentation) {
     }
 
     Helper(ImmutableHashSet.Create<object>(), root, 0);
+    writer.Flush();
   }
 
   public static string Stringify(this object root, bool showNullChildren = false) {
diff --git a/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs b/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs
index 1e9fe25f081..a9e966bfa4d 100644
--- a/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs
+++ b/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs
@@ -15,6 +15,7 @@ public class TestNotificationReceiver<TNotification> {
 
     public void NotificationReceived(TNotification request) {
       notifications.Enqueue(request);
+      notificationHistory.Add(request);
       availableNotifications.Release();
     }
 
@@ -29,7 +30,6 @@ public void ClearHistory() {
     public async Task<TNotification> AwaitNextNotificationAsync(CancellationToken cancellationToken) {
       await availableNotifications.WaitAsync(cancellationToken);
       if (notifications.TryDequeue(out var notification)) {
-        notificationHistory.Add(notification);
         return notification;
       }
       throw new System.InvalidOperationException("got a signal for a received notification but it was not present in the queue");
diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
index 0bd90df8ebb..15c290ccf61 100644
--- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
+++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
@@ -119,12 +119,12 @@ public IdeState CreateUnloaded(Compilation compilation) {
     }
 
     public Task<CompilationAfterParsing> ParseAsync(DafnyOptions options, Compilation compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
-      return loader.ParseAsync(options, compilation, ImmutableDictionary<Uri, VerificationTree>.Empty, cancellationToken);
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
+      return loader.ParseAsync(options, compilation, ImmutableDictionary<Uri, DocumentVerificationTree>.Empty, cancellationToken);
     }
 
     public Task<CompilationAfterResolution> ResolveAsync(DafnyOptions options, CompilationAfterParsing compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
       if (tests.CrashOnLoad) {
         throw new IOException("testing crash");
       }
diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs
index 9d9c50304a8..5c7162911aa 100644
--- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs
+++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs
@@ -1,11 +1,9 @@
 using System;
-using System.Collections.Generic;
 using System.Diagnostics;
 using System.Text.RegularExpressions;
 using Microsoft.Dafny.LanguageServer.Handlers;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Workspace;
-using Microsoft.Extensions.Configuration;
 using Microsoft.Extensions.DependencyInjection;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -14,7 +12,6 @@
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Boogie.SMTLib;
-using Microsoft.Extensions.Options;
 using Action = System.Action;
 
 namespace Microsoft.Dafny.LanguageServer {
diff --git a/Source/DafnyLanguageServer/Language/CachingParser.cs b/Source/DafnyLanguageServer/Language/CachingParser.cs
index d89aa103164..74397d15705 100644
--- a/Source/DafnyLanguageServer/Language/CachingParser.cs
+++ b/Source/DafnyLanguageServer/Language/CachingParser.cs
@@ -28,7 +28,6 @@ public override Program ParseFiles(string programName, IReadOnlyList<DafnyFile>
 
   protected override DfyParseResult ParseFile(DafnyOptions options, Func<TextReader> getReader,
     Uri uri, CancellationToken cancellationToken) {
-
     using var reader = getReader();
     var (newReader, hash) = ComputeHashFromReader(uri, reader, HashAlgorithm.Create("SHA256")!);
     if (!parseCache.TryGet(hash, out var result)) {
diff --git a/Source/DafnyLanguageServer/Language/IVerificationProgressReporter.cs b/Source/DafnyLanguageServer/Language/IVerificationProgressReporter.cs
index b0f13d032ac..0e253f5c81d 100644
--- a/Source/DafnyLanguageServer/Language/IVerificationProgressReporter.cs
+++ b/Source/DafnyLanguageServer/Language/IVerificationProgressReporter.cs
@@ -7,7 +7,7 @@ namespace Microsoft.Dafny.LanguageServer.Language {
   /// A callback interface to report verification progress
   /// </summary>
   public interface IVerificationProgressReporter {
-    void RecomputeVerificationTrees(CompilationAfterResolution compilation);
+    void RecomputeVerificationTrees(CompilationAfterParsing compilation);
     void ReportRealtimeDiagnostics(CompilationAfterParsing compilation, Uri uri, bool verificationStarted);
 
     void ReportImplementationsBeforeVerification(CompilationAfterResolution compilation, ICanVerify canVerify, Implementation[] implementations);
diff --git a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs
index 007daa89941..8ab2b9c92c2 100644
--- a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs
+++ b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs
@@ -38,7 +38,6 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv
           new IdeStateObserver(serviceProvider.GetRequiredService<ILogger<IdeStateObserver>>(),
             serviceProvider.GetRequiredService<ITelemetryPublisher>(),
             serviceProvider.GetRequiredService<INotificationPublisher>(),
-            serviceProvider.GetRequiredService<ITextDocumentLoader>(),
             compilation))
         .AddSingleton<IVerificationProgressReporter, VerificationProgressReporter>()
         .AddSingleton(CreateVerifier)
diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs
index cb32f591ac0..96fb33032aa 100644
--- a/Source/DafnyLanguageServer/ServerCommand.cs
+++ b/Source/DafnyLanguageServer/ServerCommand.cs
@@ -7,6 +7,7 @@
 namespace Microsoft.Dafny.LanguageServer;
 
 public class ServerCommand : ICommandSpec {
+  public const int DefaultThrottleTime = 100;
   public static readonly ServerCommand Instance = new();
 
   private ServerCommand() {
@@ -20,7 +21,8 @@ static ServerCommand() {
       GhostIndicators,
       LineVerificationStatus,
       VerifySnapshots,
-      UseCaching
+      UseCaching,
+      UpdateThrottling
     );
   }
 
@@ -29,6 +31,11 @@ static ServerCommand() {
     IsHidden = true
   };
 
+  public static readonly Option<int> UpdateThrottling = new("--update-throttling", () => DefaultThrottleTime,
+    @"How many milliseconds the server will wait before sending new document updates to the client. Higher values reduce bandwidth at the cost of responsiveness".TrimStart()) {
+    IsHidden = true
+  };
+
   public static readonly Option<bool> GhostIndicators = new("--notify-ghostness",
     @"
 (experimental, API will change)
@@ -64,6 +71,7 @@ related locations
     LineVerificationStatus,
     VerifySnapshots,
     UseCaching,
+    UpdateThrottling,
     DeveloperOptionBag.BoogiePrint,
     CommonOptionBag.EnforceDeterminism,
     CommonOptionBag.UseJavadocLikeDocstringRewriterOption
diff --git a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs
index 68fe980d4c0..f7d9e0bcaa3 100644
--- a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs
+++ b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs
@@ -22,7 +22,7 @@ public delegate CompilationManager CreateCompilationManager(
   DafnyOptions options,
   ExecutionEngine boogieEngine,
   Compilation compilation,
-  IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees);
+  IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees);
 
 /// <summary>
 /// The compilation of a single document version.
@@ -41,7 +41,7 @@ public class CompilationManager {
   private readonly IVerificationProgressReporter verificationProgressReporter;
 
   // TODO CompilationManager shouldn't be aware of migration
-  private readonly IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees;
+  private readonly IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees;
 
   private TaskCompletionSource started = new();
   private readonly IScheduler verificationUpdateScheduler = new EventLoopScheduler();
@@ -66,7 +66,7 @@ public CompilationManager(
     DafnyOptions options,
     ExecutionEngine boogieEngine,
     Compilation compilation,
-    IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees
+    IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees
     ) {
     this.options = options;
     startingCompilation = compilation;
@@ -93,14 +93,20 @@ public void Start() {
   private async Task<CompilationAfterParsing> ParseAsync() {
     try {
       await started.Task;
-      var parsedCompilation = await documentLoader.ParseAsync(options, startingCompilation, migratedVerificationTrees, cancellationSource.Token);
+      var parsedCompilation = await documentLoader.ParseAsync(options, startingCompilation, migratedVerificationTrees,
+        cancellationSource.Token);
+      verificationProgressReporter.RecomputeVerificationTrees(parsedCompilation);
       foreach (var root in parsedCompilation.RootUris) {
         verificationProgressReporter.ReportRealtimeDiagnostics(parsedCompilation, root, false);
       }
+
       compilationUpdates.OnNext(parsedCompilation);
-      logger.LogDebug($"Passed parsedCompilation to documentUpdates.OnNext, resolving ParsedCompilation task for version {parsedCompilation.Version}.");
+      logger.LogDebug(
+        $"Passed parsedCompilation to documentUpdates.OnNext, resolving ParsedCompilation task for version {parsedCompilation.Version}.");
       return parsedCompilation;
 
+    } catch (OperationCanceledException) {
+      throw;
     } catch (Exception e) {
       compilationUpdates.OnError(e);
       throw;
@@ -123,6 +129,8 @@ private async Task<CompilationAfterResolution> ResolveAsync() {
       logger.LogDebug($"Passed resolvedCompilation to documentUpdates.OnNext, resolving ResolvedCompilation task for version {resolvedCompilation.Version}.");
       return resolvedCompilation;
 
+    } catch (OperationCanceledException) {
+      throw;
     } catch (Exception e) {
       compilationUpdates.OnError(e);
       throw;
@@ -178,6 +186,9 @@ public async Task<bool> VerifySymbol(FilePosition verifiableLocation, bool actua
           g => g.Key,
           g => (IReadOnlyList<IImplementationTask>)g.ToList());
       });
+    } catch (OperationCanceledException) {
+      verificationCompleted.TrySetCanceled();
+      throw;
     } catch (Exception e) {
       verificationCompleted.TrySetException(e);
       compilationUpdates.OnError(e);
diff --git a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs
index 8ad86d8a4b4..00f68856315 100644
--- a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs
+++ b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs
@@ -46,7 +46,7 @@ public IdeState InitialIdeState(Compilation initialCompilation, DafnyOptions opt
         SymbolTable.Empty(), LegacySignatureAndCompletionTable.Empty(options, initialCompilation.Project), new(),
         Array.Empty<Counterexample>(),
         ImmutableDictionary<Uri, IReadOnlyList<Range>>.Empty,
-        initialCompilation.RootUris.ToDictionary(uri => uri, uri => (VerificationTree)new DocumentVerificationTree(program, uri))
+        initialCompilation.RootUris.ToDictionary(uri => uri, uri => new DocumentVerificationTree(program, uri))
       ));
     }
 
diff --git a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs
index 8ddddbcb47f..4758b5294b5 100644
--- a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs
+++ b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs
@@ -11,12 +11,12 @@ namespace Microsoft.Dafny.LanguageServer.Workspace;
 
 public class CompilationAfterParsing : Compilation {
   public IReadOnlyDictionary<Uri, List<DafnyDiagnostic>> ResolutionDiagnostics { get; set; }
-  public Dictionary<Uri, VerificationTree> VerificationTrees { get; }
+  public Dictionary<Uri, DocumentVerificationTree> VerificationTrees { get; }
 
   public CompilationAfterParsing(Compilation compilation,
     Program program,
     IReadOnlyDictionary<Uri, List<DafnyDiagnostic>> diagnostics,
-    Dictionary<Uri, VerificationTree> verificationTrees)
+    Dictionary<Uri, DocumentVerificationTree> verificationTrees)
     : base(compilation.Version, compilation.Project, compilation.RootUris) {
     ResolutionDiagnostics = diagnostics;
     VerificationTrees = verificationTrees;
diff --git a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs
index 34f6b3fec61..f6b8df0c6d4 100644
--- a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs
+++ b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs
@@ -7,6 +7,8 @@
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
@@ -72,7 +74,6 @@ IdeVerificationResult MergeResults(IEnumerable<IdeVerificationResult> results) {
   }
 
   public override IdeState ToIdeState(IdeState previousState) {
-
     IdeVerificationResult MergeVerifiable(ICanVerify canVerify) {
       var range = canVerify.NameToken.GetLspRange();
       var previousForCanVerify = previousState.GetVerificationResults(canVerify.NameToken.Uri).GetValueOrDefault(range) ??
@@ -108,7 +109,7 @@ IdeVerificationResult MergeVerifiable(ICanVerify canVerify) {
       SignatureAndCompletionTable = SignatureAndCompletionTable.Resolved ? SignatureAndCompletionTable : previousState.SignatureAndCompletionTable,
       GhostRanges = GhostDiagnostics,
       Counterexamples = new List<Counterexample>(Counterexamples),
-      VerificationTrees = VerificationTrees.ToDictionary(kv => kv.Key, kv => kv.Value.GetCopyForNotification()),
+      VerificationTrees = VerificationTrees.ToDictionary(kv => kv.Key, kv => (DocumentVerificationTree)kv.Value.GetCopyForNotification()),
       VerificationResults = Verifiables.GroupBy(l => l.NameToken.Uri).ToDictionary(k => k.Key,
         k => k.GroupBy(l => l.NameToken.GetLspRange()).ToDictionary(
           l => l.Key,
diff --git a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
index efa5c29dd79..734dfce71fc 100644
--- a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
@@ -22,10 +22,10 @@ public interface ITextDocumentLoader {
     IdeState CreateUnloaded(Compilation compilation);
 
     Task<CompilationAfterParsing> ParseAsync(DafnyOptions options, Compilation compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken);
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken);
 
     Task<CompilationAfterResolution> ResolveAsync(DafnyOptions options, CompilationAfterParsing compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees,
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees,
       CancellationToken cancellationToken);
   }
 }
diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs
index 7b6bfffe19d..ed44d59fca0 100644
--- a/Source/DafnyLanguageServer/Workspace/IdeState.cs
+++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs
@@ -5,6 +5,7 @@
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using OmniSharp.Extensions.LanguageServer.Protocol;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -32,9 +33,48 @@ public record IdeState(
   Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> VerificationResults,
   IReadOnlyList<Counterexample> Counterexamples,
   IReadOnlyDictionary<Uri, IReadOnlyList<Range>> GhostRanges,
-  IReadOnlyDictionary<Uri, VerificationTree> VerificationTrees
+  IReadOnlyDictionary<Uri, DocumentVerificationTree> VerificationTrees
 ) {
 
+  public IdeState Migrate(Migrator migrator, int version) {
+    var migratedVerificationTrees = VerificationTrees.ToDictionary(
+      kv => kv.Key, kv =>
+        (DocumentVerificationTree)migrator.RelocateVerificationTree(kv.Value));
+    return this with {
+      Version = version,
+      VerificationResults = MigrateImplementationViews(migrator, VerificationResults),
+      SignatureAndCompletionTable = migrator.MigrateSymbolTable(SignatureAndCompletionTable),
+      VerificationTrees = migratedVerificationTrees
+    };
+  }
+
+  private Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> MigrateImplementationViews(Migrator migrator,
+    Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> oldVerificationDiagnostics) {
+    return oldVerificationDiagnostics.ToDictionary(kv => kv.Key, kv => {
+      var result = new Dictionary<Range, IdeVerificationResult>();
+      foreach (var entry in kv.Value) {
+        var newOuterRange = migrator.MigrateRange(entry.Key);
+        if (newOuterRange == null) {
+          continue;
+        }
+
+        var newValue = new Dictionary<string, IdeImplementationView>();
+        foreach (var innerEntry in entry.Value.Implementations) {
+          var newInnerRange = migrator.MigrateRange(innerEntry.Value.Range);
+          if (newInnerRange != null) {
+            newValue.Add(innerEntry.Key, innerEntry.Value with {
+              Range = newInnerRange,
+              Diagnostics = migrator.MigrateDiagnostics(innerEntry.Value.Diagnostics)
+            });
+          }
+        }
+
+        result.Add(newOuterRange, entry.Value with { Implementations = newValue });
+      }
+
+      return result;
+    });
+  }
 
   public IReadOnlyDictionary<Range, IdeVerificationResult> GetVerificationResults(Uri uri) {
     return VerificationResults.GetValueOrDefault(uri) ??
diff --git a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
index 2fd77fb5817..3edbbe09dd6 100644
--- a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
+++ b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
@@ -2,9 +2,7 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.Immutable;
-using System.Linq;
-using System.Threading;
-using Microsoft.Boogie;
+using System.Reactive;
 using Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -12,35 +10,33 @@
 
 namespace Microsoft.Dafny.LanguageServer.Workspace;
 
-public delegate IdeStateObserver CreateIdeStateObserver(Compilation compilation);
+public delegate IdeStateObserver CreateIdeStateObserver(IdeState initialState);
 
-public class IdeStateObserver : IObserver<IdeState> {
+public class IdeStateObserver : IObserver<IdeState> { // Inheriting from ObserverBase prevents this observer from recovering after a problem
   private readonly ILogger logger;
   private readonly ITelemetryPublisher telemetryPublisher;
   private readonly INotificationPublisher notificationPublisher;
-  private readonly ITextDocumentLoader loader;
-  private readonly Compilation compilation;
 
   private readonly object lastPublishedStateLock = new();
+  private readonly IdeState initialState;
 
   public IdeState LastPublishedState { get; private set; }
 
   public IdeStateObserver(ILogger logger,
     ITelemetryPublisher telemetryPublisher,
     INotificationPublisher notificationPublisher,
-    ITextDocumentLoader loader,
-    Compilation compilation) {
-    LastPublishedState = loader.CreateUnloaded(compilation);
+    IdeState initialState) {
+    this.initialState = initialState;
+    LastPublishedState = initialState;
     this.logger = logger;
     this.telemetryPublisher = telemetryPublisher;
     this.notificationPublisher = notificationPublisher;
-    this.loader = loader;
-    this.compilation = compilation;
   }
 
   public void OnCompleted() {
-    var initialCompilation = new Compilation(LastPublishedState.Version + 1, LastPublishedState.Compilation.Project, compilation.RootUris);
-    var ideState = loader.CreateUnloaded(initialCompilation);
+    var ideState = initialState with {
+      Version = LastPublishedState.Version + 1
+    };
 #pragma warning disable VSTHRD002
     notificationPublisher.PublishNotifications(LastPublishedState, ideState).Wait();
 #pragma warning restore VSTHRD002
@@ -48,11 +44,6 @@ public void OnCompleted() {
   }
 
   public void OnError(Exception exception) {
-    if (exception is OperationCanceledException) {
-      logger.LogDebug("document processing cancelled.");
-      return;
-    }
-
     var internalErrorDiagnostic = new Diagnostic {
       Message =
         "Dafny encountered an internal error. Please report it at <https://github.com/dafny-lang/dafny/issues>.\n" +
@@ -61,7 +52,7 @@ public void OnError(Exception exception) {
       Range = new Range(0, 0, 0, 1)
     };
     var documentToPublish = LastPublishedState with {
-      ResolutionDiagnostics = ImmutableDictionary<Uri, IReadOnlyList<Diagnostic>>.Empty.Add(compilation.Project.Uri, new[] { internalErrorDiagnostic })
+      ResolutionDiagnostics = ImmutableDictionary<Uri, IReadOnlyList<Diagnostic>>.Empty.Add(initialState.Compilation.Uri.ToUri(), new[] { internalErrorDiagnostic })
     };
 
     OnNext(documentToPublish);
@@ -82,50 +73,14 @@ public void OnNext(IdeState snapshot) {
       notificationPublisher.PublishNotifications(LastPublishedState, snapshot).Wait();
 #pragma warning restore VSTHRD002
       LastPublishedState = snapshot;
-      logger.LogDebug($"Updated LastPublishedState to version {snapshot.Version}, uri {compilation.Uri}");
+      logger.LogDebug($"Updated LastPublishedState to version {snapshot.Version}, uri {initialState.Compilation.Uri.ToUri()}");
     }
   }
 
   public void Migrate(Migrator migrator, int version) {
     lock (lastPublishedStateLock) {
-      var migratedVerificationTrees = LastPublishedState.VerificationTrees.ToDictionary(
-        kv => kv.Key, kv =>
-          migrator.RelocateVerificationTree(kv.Value));
-      LastPublishedState = LastPublishedState with {
-        Version = version,
-        VerificationResults = MigrateImplementationViews(migrator, LastPublishedState.VerificationResults),
-        SignatureAndCompletionTable = migrator.MigrateSymbolTable(LastPublishedState.SignatureAndCompletionTable),
-        VerificationTrees = migratedVerificationTrees
-      };
-      logger.LogDebug($"Migrated LastPublishedState to version {version}, uri {compilation.Uri}");
+      LastPublishedState = LastPublishedState.Migrate(migrator, version);
+      logger.LogDebug($"Migrated LastPublishedState to version {version}, uri {initialState.Compilation.Uri.ToUri()}");
     }
   }
-
-  private Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> MigrateImplementationViews(Migrator migrator,
-      Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> oldVerificationDiagnostics) {
-    return oldVerificationDiagnostics.ToDictionary(kv => kv.Key, kv => {
-      var result = new Dictionary<Range, IdeVerificationResult>();
-      foreach (var entry in kv.Value) {
-        var newOuterRange = migrator.MigrateRange(entry.Key);
-        if (newOuterRange == null) {
-          continue;
-        }
-
-        var newValue = new Dictionary<string, IdeImplementationView>();
-        foreach (var innerEntry in entry.Value.Implementations) {
-          var newInnerRange = migrator.MigrateRange(innerEntry.Value.Range);
-          if (newInnerRange != null) {
-            newValue.Add(innerEntry.Key, innerEntry.Value with {
-              Range = newInnerRange,
-              Diagnostics = migrator.MigrateDiagnostics(innerEntry.Value.Diagnostics)
-            });
-          }
-        }
-
-        result.Add(newOuterRange, entry.Value with { Implementations = newValue });
-      }
-
-      return result;
-    });
-  }
 }
diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
index 9f2e39308c7..aca88cf7681 100644
--- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
+++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
@@ -4,6 +4,7 @@
 using System.IO;
 using System.Linq;
 using System.Numerics;
+using System.Reactive;
 using System.Reactive.Disposables;
 using System.Reactive.Linq;
 using System.Threading;
@@ -60,6 +61,7 @@ public class ProjectManager : IDisposable {
   private readonly CreateCompilationManager createCompilationManager;
   private readonly ExecutionEngine boogieEngine;
   private readonly IFileSystem fileSystem;
+  private Lazy<IdeState> latestIdeState;
 
   public ProjectManager(
     DafnyOptions serverOptions,
@@ -84,11 +86,13 @@ public ProjectManager(
 
     options = DetermineProjectOptions(project, serverOptions);
     options.Printer = new OutputLogger(logger);
-
     var initialCompilation = CreateInitialCompilation();
-    observer = createIdeStateObserver(initialCompilation);
+    var initialIdeState = initialCompilation.InitialIdeState(initialCompilation, options);
+    latestIdeState = new Lazy<IdeState>(initialIdeState);
+
+    observer = createIdeStateObserver(initialIdeState);
     CompilationManager = createCompilationManager(
-        options, boogieEngine, initialCompilation, ImmutableDictionary<Uri, VerificationTree>.Empty
+        options, boogieEngine, initialCompilation, ImmutableDictionary<Uri, DocumentVerificationTree>.Empty
     );
 
     observerSubscription = Disposable.Empty;
@@ -103,10 +107,14 @@ private Compilation CreateInitialCompilation() {
   private const int MaxRememberedChangedVerifiables = 5;
 
   public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
-    var changeProcessor = createMigrator(documentChange, CancellationToken.None);
-    observer.Migrate(changeProcessor, version + 1);
-    var lastPublishedState = observer.LastPublishedState;
-    var migratedVerificationTrees = lastPublishedState.VerificationTrees;
+    var migrator = createMigrator(documentChange, CancellationToken.None);
+    Lazy<IdeState> lazyPreviousCompilationLastIdeState = latestIdeState;
+    latestIdeState = new Lazy<IdeState>(() => {
+      // If we migrate the observer before accessing latestIdeState, we can be sure it's migrated before it receives new events.
+      observer.Migrate(migrator, version + 1);
+      return lazyPreviousCompilationLastIdeState.Value.Migrate(migrator, version + 1);
+    });
+    StartNewCompilation();
 
     lock (RecentChanges) {
       var newChanges = documentChange.ContentChanges.Where(c => c.Range != null).
@@ -115,7 +123,7 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
           Uri = documentChange.TextDocument.Uri
         });
       var migratedChanges = RecentChanges.Select(location => {
-        var newRange = changeProcessor.MigrateRange(location.Range);
+        var newRange = migrator.MigrateRange(location.Range);
         if (newRange == null) {
           return null;
         }
@@ -126,32 +134,34 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
       }).Where(r => r != null);
       RecentChanges = newChanges.Concat(migratedChanges).Take(MaxRememberedChanges).ToList()!;
     }
-
-    StartNewCompilation(migratedVerificationTrees, lastPublishedState);
     TriggerVerificationForFile(documentChange.TextDocument.Uri.ToUri());
   }
 
-  private void StartNewCompilation(IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees,
-    IdeState lastPublishedState) {
+  private void StartNewCompilation() {
     version++;
     logger.LogDebug("Clearing result for workCompletedForCurrentVersion");
 
+    Lazy<IdeState> migratedLazyPreviousCompilationLastIdeState = latestIdeState;
+    observerSubscription.Dispose();
+
     CompilationManager.CancelPendingUpdates();
     CompilationManager = createCompilationManager(
       options,
       boogieEngine,
       CreateInitialCompilation(),
-      migratedVerificationTrees);
+      latestIdeState.Value.VerificationTrees);
 
-    observerSubscription.Dispose();
     var migratedUpdates = CompilationManager.CompilationUpdates.Select(document =>
-      document.ToIdeState(lastPublishedState));
-    observerSubscription = migratedUpdates.Subscribe(observer);
+      latestIdeState = new Lazy<IdeState>(() => document.ToIdeState(migratedLazyPreviousCompilationLastIdeState.Value)));
+    var throttleTime = options.Get(ServerCommand.UpdateThrottling);
+    var throttledUpdates = throttleTime == 0 ? migratedUpdates : migratedUpdates.Sample(TimeSpan.FromMilliseconds(throttleTime));
+    observerSubscription = throttledUpdates.
+      Select(x => x.Value).Subscribe(observer);
 
     CompilationManager.Start();
   }
 
-  public void TriggerVerificationForFile(Uri triggeringFile) {
+  private void TriggerVerificationForFile(Uri triggeringFile) {
     if (AutomaticVerificationMode is VerifyOnMode.Change or VerifyOnMode.ChangeProject) {
       var _ = VerifyEverythingAsync(AutomaticVerificationMode == VerifyOnMode.Change ? triggeringFile : null);
     } else {
@@ -216,8 +226,8 @@ public async Task<IdeState> GetSnapshotAfterParsingAsync() {
       logger.LogDebug($"GetSnapshotAfterResolutionAsync caught OperationCanceledException for parsed compilation {Project.Uri}");
     }
 
-    logger.LogDebug($"GetSnapshotAfterParsingAsync returns state version {observer.LastPublishedState.Version}");
-    return observer.LastPublishedState;
+    logger.LogDebug($"GetSnapshotAfterParsingAsync returns state version {latestIdeState.Value.Version}");
+    return latestIdeState.Value;
   }
 
   public async Task<IdeState> GetStateAfterResolutionAsync() {
@@ -229,8 +239,8 @@ public async Task<IdeState> GetStateAfterResolutionAsync() {
       return await GetSnapshotAfterParsingAsync();
     }
 
-    logger.LogDebug($"GetStateAfterResolutionAsync returns state version {observer.LastPublishedState.Version}");
-    return observer.LastPublishedState;
+    logger.LogDebug($"GetStateAfterResolutionAsync returns state version {latestIdeState.Value.Version}");
+    return latestIdeState.Value;
   }
 
   public async Task<IdeState> GetIdeStateAfterVerificationAsync() {
@@ -239,7 +249,7 @@ public async Task<IdeState> GetIdeStateAfterVerificationAsync() {
     } catch (OperationCanceledException) {
     }
 
-    return observer.LastPublishedState;
+    return latestIdeState.Value;
   }
 
 
@@ -328,11 +338,9 @@ IntervalTree<Position, Position> GetTree(Uri uri) {
 
   public void OpenDocument(Uri uri, bool triggerCompilation) {
     Interlocked.Increment(ref openFileCount);
-    var lastPublishedState = observer.LastPublishedState;
-    var migratedVerificationTrees = lastPublishedState.VerificationTrees;
 
     if (triggerCompilation) {
-      StartNewCompilation(migratedVerificationTrees, lastPublishedState);
+      StartNewCompilation();
       TriggerVerificationForFile(uri);
     }
   }
diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
index f5695afd73a..450dca15f5b 100644
--- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
@@ -56,7 +56,7 @@ public IdeState CreateUnloaded(Compilation compilation) {
     }
 
     public async Task<CompilationAfterParsing> ParseAsync(DafnyOptions options, Compilation compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
 #pragma warning disable CS1998
       return await await DafnyMain.LargeStackFactory.StartNew(
         async () => ParseInternal(options, compilation, migratedVerificationTrees, cancellationToken), cancellationToken
@@ -65,7 +65,7 @@ public async Task<CompilationAfterParsing> ParseAsync(DafnyOptions options, Comp
     }
 
     private CompilationAfterParsing ParseInternal(DafnyOptions options, Compilation compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees,
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees,
       CancellationToken cancellationToken) {
       var project = compilation.Project;
       var errorReporter = new DiagnosticErrorReporter(options, project.Uri);
@@ -79,17 +79,16 @@ private CompilationAfterParsing ParseInternal(DafnyOptions options, Compilation
 
     public async Task<CompilationAfterResolution> ResolveAsync(DafnyOptions options,
       CompilationAfterParsing compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees,
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees,
       CancellationToken cancellationToken) {
 #pragma warning disable CS1998
       return await await DafnyMain.LargeStackFactory.StartNew(
-        async () => ResolveInternal(compilation, migratedVerificationTrees, cancellationToken), cancellationToken
+        async () => ResolveInternal(compilation, migratedVerificationTrees, cancellationToken), cancellationToken);
 #pragma warning restore CS1998
-        );
     }
 
     private CompilationAfterResolution ResolveInternal(CompilationAfterParsing compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
 
       var program = compilation.Program;
       var errorReporter = (DiagnosticErrorReporter)program.Reporter;
@@ -144,7 +143,7 @@ private IdeState CreateDocumentWithEmptySymbolTable(Compilation compilation,
         new(),
         Array.Empty<Counterexample>(),
         ImmutableDictionary<Uri, IReadOnlyList<Range>>.Empty,
-      ImmutableDictionary<Uri, VerificationTree>.Empty
+      ImmutableDictionary<Uri, DocumentVerificationTree>.Empty
       );
     }
   }
diff --git a/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs b/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
index c9d0968d440..51da0d929e4 100644
--- a/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
+++ b/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
@@ -28,15 +28,21 @@ public VerificationProgressReporter(ILogger<VerificationProgressReporter> logger
   /// Fills up the document with empty verification diagnostics, one for each top-level declarations
   /// Possibly migrates previous diagnostics
   /// </summary>
-  public void RecomputeVerificationTrees(CompilationAfterResolution compilation) {
-    foreach (var tree in compilation.VerificationTrees.Values) {
-      UpdateTree(options, compilation, tree);
+  public void RecomputeVerificationTrees(CompilationAfterParsing compilation) {
+    foreach (var uri in compilation.VerificationTrees.Keys) {
+      compilation.VerificationTrees[uri] = UpdateTree(options, compilation, compilation.VerificationTrees[uri]);
     }
   }
 
-  public static void UpdateTree(DafnyOptions options, CompilationAfterParsing parsedCompilation, VerificationTree rootVerificationTree) {
+  private static DocumentVerificationTree UpdateTree(DafnyOptions options, CompilationAfterParsing parsedCompilation, DocumentVerificationTree rootVerificationTree) {
     var previousTrees = rootVerificationTree.Children;
 
+    if (parsedCompilation is not CompilationAfterResolution) {
+      return new DocumentVerificationTree(parsedCompilation.Program, rootVerificationTree.Uri) {
+        Children = rootVerificationTree.Children
+      };
+    }
+
     List<VerificationTree> result = new List<VerificationTree>();
 
     HashSet<Position> recordedPositions = new HashSet<Position>();
@@ -151,7 +157,9 @@ void AddAndPossiblyMigrateVerificationTree(VerificationTree verificationTree) {
       }
     }
 
-    rootVerificationTree.Children = result;
+    return new DocumentVerificationTree(parsedCompilation.Program, rootVerificationTree.Uri) {
+      Children = result
+    };
   }
 
   /// <summary>
diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj
index 7d2c524f988..d22194db572 100644
--- a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj
+++ b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj
@@ -13,7 +13,7 @@
 
   <ItemGroup>
     <PackageReference Include="DiffPlex" Version="1.7.0" />
-    <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.11.0" />
+    <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.1.0" />
     <PackageReference Include="xunit" Version="2.4.2" />
     <PackageReference Include="xunit.runner.visualstudio" Version="2.4.3">
       <IncludeAssets>runtime; build; native; contentfiles; analyzers; buildtransitive</IncludeAssets>
@@ -26,6 +26,7 @@
   </ItemGroup>
 
   <ItemGroup>
+    <ProjectReference Include="..\DafnyCore.Test\DafnyCore.Test.csproj" />
     <ProjectReference Include="..\DafnyDriver\DafnyDriver.csproj" />
   </ItemGroup>
 
diff --git a/Source/DafnyPipeline.Test/DocstringTest.cs b/Source/DafnyPipeline.Test/DocstringTest.cs
index 6067370e304..50e07bf3e60 100644
--- a/Source/DafnyPipeline.Test/DocstringTest.cs
+++ b/Source/DafnyPipeline.Test/DocstringTest.cs
@@ -1,8 +1,10 @@
 #nullable enable
 using System;
 using System.Collections.Generic;
+using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
@@ -426,7 +428,7 @@ protected void DocstringWorksFor(string source, string nodeTokenValue, string? e
     }
 
     protected void DocstringWorksFor(string source, List<(string nodeTokenValue, string? expectedDocstring)> tests) {
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(output));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(output));
       var newlineTypes = Enum.GetValues(typeof(Newlines));
       foreach (Newlines newLinesType in newlineTypes) {
         currentNewlines = newLinesType;
diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs
index f8bb5395f57..14718152321 100644
--- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs
+++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs
@@ -4,6 +4,7 @@
 using System.Collections.Immutable;
 using System.IO;
 using System.Text.RegularExpressions;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
diff --git a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs
index 3d5fd272f72..bd577a9b6ac 100644
--- a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs
+++ b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs
@@ -2,6 +2,7 @@
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Microsoft.Boogie;
 using Microsoft.Dafny;
@@ -148,7 +149,7 @@ public IntraMethodVerificationStability(ITestOutputHelper testOutputHelper) {
 
     [Fact]
     public void NoUniqueLinesWhenConcatenatingUnrelatedPrograms() {
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper));
 
       var regularBoogie = GetBoogie(options, originalProgram).ToList();
       var renamedBoogie = GetBoogie(options, renamedProgram).ToList();
@@ -164,7 +165,7 @@ public void NoUniqueLinesWhenConcatenatingUnrelatedPrograms() {
 
     [Fact]
     public async Task EqualProverLogWhenReorderingProgram() {
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper));
       options.ProcsToCheck.Add("SomeMethod*");
 
       var reorderedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, reorderedProgram));
@@ -174,7 +175,7 @@ public async Task EqualProverLogWhenReorderingProgram() {
 
     [Fact]
     public async Task EqualProverLogWhenRenamingProgram() {
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper));
       options.ProcsToCheck.Add("*SomeMethod*");
 
       var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram));
@@ -185,7 +186,7 @@ public async Task EqualProverLogWhenRenamingProgram() {
     [Fact]
     public async Task EqualProverLogWhenAddingUnrelatedProgram() {
 
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper));
       options.ProcsToCheck.Add("*SomeMethod *");
 
       var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram + originalProgram));
diff --git a/Source/DafnyPipeline.Test/Issue1355.cs b/Source/DafnyPipeline.Test/Issue1355.cs
index 8ac93cd5c8e..d4f260f09f3 100644
--- a/Source/DafnyPipeline.Test/Issue1355.cs
+++ b/Source/DafnyPipeline.Test/Issue1355.cs
@@ -1,4 +1,5 @@
 using System.IO;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs
index 7cfa42bbe93..f9a4fe97b0a 100644
--- a/Source/DafnyPipeline.Test/PluginsTest.cs
+++ b/Source/DafnyPipeline.Test/PluginsTest.cs
@@ -2,6 +2,7 @@
 using System.IO;
 using System.Linq;
 using System.Reflection;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Microsoft.CodeAnalysis;
 using Microsoft.CodeAnalysis.CSharp;
diff --git a/Source/DafnyPipeline.Test/RelativePaths.cs b/Source/DafnyPipeline.Test/RelativePaths.cs
index 4d71cc07d1d..03ba9e4b93e 100644
--- a/Source/DafnyPipeline.Test/RelativePaths.cs
+++ b/Source/DafnyPipeline.Test/RelativePaths.cs
@@ -1,4 +1,5 @@
 using System.IO;
+using DafnyCore.Test;
 using Microsoft.Dafny;
 using Xunit;
 using Xunit.Abstractions;
diff --git a/Source/DafnyPipeline.Test/Trivia.cs b/Source/DafnyPipeline.Test/Trivia.cs
index be312c3e598..bd812e8b106 100644
--- a/Source/DafnyPipeline.Test/Trivia.cs
+++ b/Source/DafnyPipeline.Test/Trivia.cs
@@ -3,6 +3,7 @@
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
diff --git a/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs b/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs
deleted file mode 100644
index c8159df29ef..00000000000
--- a/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs
+++ /dev/null
@@ -1,30 +0,0 @@
-#nullable enable
-using System.IO;
-using System.Text;
-using Xunit.Abstractions;
-
-public class WriterFromOutputHelper : TextWriter {
-  private readonly ITestOutputHelper output;
-  private bool failed = false;
-
-  public WriterFromOutputHelper(ITestOutputHelper output) {
-    this.output = output;
-  }
-
-  public override void Write(char value) {
-    if (!failed) {
-      failed = true;
-      WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support.");
-    }
-  }
-
-  public override Encoding Encoding => Encoding.Default;
-
-  public override void WriteLine(string? value) {
-    output.WriteLine(value);
-  }
-
-  public override void WriteLine(string format, params object?[] arg) {
-    output.WriteLine(format, arg);
-  }
-}
\ No newline at end of file
diff --git a/Source/DafnyTestGeneration.Test/BasicTypes.cs b/Source/DafnyTestGeneration.Test/BasicTypes.cs
index a5358746ae0..2952b80bc95 100644
--- a/Source/DafnyTestGeneration.Test/BasicTypes.cs
+++ b/Source/DafnyTestGeneration.Test/BasicTypes.cs
@@ -8,6 +8,7 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny;
 using Xunit;
 using Xunit.Abstractions;
diff --git a/Source/DafnyTestGeneration.Test/Collections.cs b/Source/DafnyTestGeneration.Test/Collections.cs
index 2a02446149e..5e3f85918fc 100644
--- a/Source/DafnyTestGeneration.Test/Collections.cs
+++ b/Source/DafnyTestGeneration.Test/Collections.cs
@@ -8,6 +8,7 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny;
 using Xunit;
 using Xunit.Abstractions;
diff --git a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj
index bf8594de184..b4920e58810 100644
--- a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj
+++ b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj
@@ -7,7 +7,7 @@
     </PropertyGroup>
 
     <ItemGroup>
-        <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.11.0" />
+        <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.1.0" />
         <PackageReference Include="xunit" Version="2.4.2" />
         <PackageReference Include="xunit.extensibility.core" Version="2.4.2" />
         <PackageReference Include="xunit.runner.visualstudio" Version="2.4.3">
@@ -18,6 +18,7 @@
     </ItemGroup>
 
     <ItemGroup>
+        <ProjectReference Include="..\DafnyCore.Test\DafnyCore.Test.csproj" />
         <ProjectReference Include="..\DafnyRuntime\DafnyRuntime.csproj" />
         <ProjectReference Include="..\DafnyTestGeneration\DafnyTestGeneration.csproj" />
     </ItemGroup>
diff --git a/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs b/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs
index 3d90ded7477..664b49d5e83 100644
--- a/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs
+++ b/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs
@@ -7,6 +7,7 @@
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
+using DafnyCore.Test;
 using DafnyTestGeneration.Inlining;
 using Microsoft.Dafny;
 using Xunit;
diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs
index 8d6237b43f9..2292fe2dd73 100644
--- a/Source/DafnyTestGeneration.Test/Various.cs
+++ b/Source/DafnyTestGeneration.Test/Various.cs
@@ -8,6 +8,7 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny;
 using Xunit;
 using Xunit.Abstractions;