Fix bug that occurred when using resolution caching and replaceable m…

…odules (dafny-lang#5189)

Fixes dafny-lang#5187

### Description
Fix bug that occurred when using resolution caching in combination with
replaceable modules

### How has this been tested?
Added a language server test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs

@@ -28,7 +28,9 @@ public ModuleQualifiedId(List<Name> path) {
 
   public ModuleQualifiedId(Cloner cloner, ModuleQualifiedId original) {
     Path = original.Path.Select(n => n.Clone(cloner)).ToList();
-    Root = original.Root;
+    if (cloner.CloneResolvedFields) {
+      Root = original.Root;
+    }
   }
 
   public string RootName() {

Source/DafnyCore/Resolver/ProgramResolver.cs

@@ -215,6 +215,12 @@ private void CheckDuplicateModuleNames(Program program) {
   }
 
   protected void InstantiateReplaceableModules(Program dafnyProgram) {
+    foreach (var compiledModule in dafnyProgram.Modules()) {
+      // This is a workaround for the problem that the IDE caches resolved modules,
+      // So this field might still be set from a previous compilation.
+      // Better solution is described here: https://github.com/dafny-lang/dafny/issues/5188
+      compiledModule.Replacement = null;
+    }
     foreach (var compiledModule in dafnyProgram.Modules().OrderByDescending(m => m.Height)) {
       if (compiledModule.Implements is { Kind: ImplementationKind.Replacement }) {
         var target = compiledModule.Implements.Target.Def;

Source/DafnyLanguageServer.Test/ProjectFiles/StandardLibrary.cs

@@ -0,0 +1,34 @@
+using System.IO;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Extensions.Logging;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles;
+
+public class StandardLibrary : ClientBasedLanguageServerTest {
+
+  [Fact]
+  public async Task EditWhenUsingStandardLibrary() {
+    var projectFile = @"
+[options]
+standard-libraries=true
+";
+    var program = @"
+method Foo() ensures false { }
+".TrimStart();
+    var path = Path.GetRandomFileName();
+    var project = CreateAndOpenTestDocument(projectFile, Path.Combine(path, DafnyProject.FileName));
+    var document = CreateAndOpenTestDocument(program, Path.Combine(path, "EditWhenUsingStandardLibrary.dfy"));
+    var diagnostics1 = await GetLastDiagnostics(document);
+    Assert.Single(diagnostics1);
+    ApplyChange(ref document, new Range(0, 0, 1, 0), "method Bar() ensures true { }");
+    var diagnostics2 = await GetLastDiagnostics(document);
+    Assert.Empty(diagnostics2);
+  }
+
+  public StandardLibrary(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information) : base(output, dafnyLogLevel) {
+  }
+}

Source/DafnyLanguageServer/DafnyLanguageServer.cs

@@ -57,16 +57,16 @@ private static void PublishSolverPath(ILanguageServer server) {
         var proverOptions = new SMTLibSolverOptions(options);
         proverOptions.Parse(options.ProverOptions);
         solverPath = proverOptions.ExecutablePath();
-        HandleZ3Version(telemetryPublisher, proverOptions);
+        HandleZ3Version(telemetryPublisher, solverPath);
       } catch (Exception e) {
         solverPath = $"Error while determining solver path: {e}";
       }
 
       telemetryPublisher.PublishSolverPath(solverPath);
     }
 
-    private static void HandleZ3Version(TelemetryPublisherBase telemetryPublisher, SMTLibSolverOptions proverOptions) {
-      var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
+    private static void HandleZ3Version(TelemetryPublisherBase telemetryPublisher, string solverPath) {
+      var z3Version = DafnyOptions.GetZ3Version(solverPath);
       if (z3Version is null) {
         return;
       }