chore: Update Windows CI runners to windows-2022

.github/workflows/release-downloads-nuget.yml

@@ -18,7 +18,7 @@ on:
 
 env:
   dotnet-version: 8.0.x # SDK Version for running Dafny (TODO: should this be an older version?)
-  z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02
+  z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2025-07-02
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/release-downloads.yml

@@ -59,8 +59,8 @@ jobs:
     ## Record versions, checking that dafny runs
     - name: Versions
       run: |
-        dafny/z3/bin/z3-4.8.5 -version
         dafny/z3/bin/z3-4.12.1 -version
+        dafny/z3/bin/z3-4.14.1 -version
         dafny/dafny -version
 
     ## Check that a simple program compiles and runs on each supported platform

Makefile

@@ -60,34 +60,34 @@ refman-release: exe
 
 z3-mac:
 	mkdir -p "${DIR}"/Binaries/z3/bin
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip
-	unzip z3-4.12.1-x64-macos-11-bin.zip
-	rm z3-4.12.1-x64-macos-11-bin.zip
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
-	unzip z3-4.8.5-x64-macos-11-bin.zip
-	rm z3-4.8.5-x64-macos-11-bin.zip
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2025-07-02/z3-4.14.1-x64-macos-13-bin.zip
+	unzip z3-4.14.1-x64-macos-13-bin.zip
+	rm z3-4.14.1-x64-macos-13-bin.zip
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2025-07-02/z3-4.12.1-x64-macos-13-bin.zip
+	unzip z3-4.12.1-x64-macos-13-bin.zip
+	rm z3-4.12.1-x64-macos-13-bin.zip
 	mv z3-* "${DIR}"/Binaries/z3/bin/
 	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
 
 z3-mac-arm:
 	mkdir -p "${DIR}"/Binaries/z3/bin
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-arm64-macos-11-bin.zip
-	unzip z3-4.12.1-arm64-macos-11-bin.zip
-	rm z3-4.12.1-arm64-macos-11-bin.zip
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
-	unzip z3-4.8.5-x64-macos-11-bin.zip
-	rm z3-4.8.5-x64-macos-11-bin.zip
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2025-07-02/z3-4.14.1-arm64-macos-13-bin.zip
+	unzip z3-4.14.1-arm64-macos-13-bin.zip
+	rm z3-4.14.1-arm64-macos-13-bin.zip
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2025-07-02/z3-4.12.1-arm64-macos-13-bin.zip
+	unzip z3-4.12.1-arm64-macos-13-bin.zip
+	rm z3-4.12.1-arm64-macos-13-bin.zip
 	mv z3-* "${DIR}"/Binaries/z3/bin/
 	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
 
 z3-ubuntu:
 	mkdir -p "${DIR}"/Binaries/z3/bin
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
-	unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
-	rm z3-4.12.1-x64-ubuntu-20.04-bin.zip
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-ubuntu-20.04-bin.zip
-	unzip z3-4.8.5-x64-ubuntu-20.04-bin.zip
-	rm z3-4.8.5-x64-ubuntu-20.04-bin.zip
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2025-07-02/z3-4.14.1-x64-ubuntu-22.04-bin.zip
+	unzip z3-4.14.1-x64-ubuntu-22.04-bin.zip
+	rm z3-4.14.1-x64-ubuntu-22.04-bin.zip
+	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2025-07-02/z3-4.12.1-x64-ubuntu-22.04-bin.zip
+	unzip z3-4.12.1-x64-ubuntu-22.04-bin.zip
+	rm z3-4.12.1-x64-ubuntu-22.04-bin.zip
 	mv z3-* "${DIR}"/Binaries/z3/bin/
 	chmod +x "${DIR}"/Binaries/z3/bin/z3-*
 

Scripts/package.py

@@ -19,8 +19,8 @@
 
 # Configuration
 
-Z3_VERSIONS = [ "4.8.5", "4.12.1" ]
-Z3_URL_BASE = "https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02"
+Z3_VERSIONS = [ "4.12.1", "4.14.1" ]
+Z3_URL_BASE = "https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2025-07-02"
 
 ## How many times we allow ourselves to try to download Z3
 Z3_MAX_DOWNLOAD_ATTEMPTS = 5
@@ -287,9 +287,9 @@ def main():
 
     # Z3
     flush("* Downloading Z3 releases")
-    releases = [ Release("macos-11",       "x64", args.version, args.out),
-                 Release("macos-11",     "arm64", args.version, args.out),
-                 Release("ubuntu-20.04",   "x64", args.version, args.out),
+    releases = [ Release("macos-13",       "x64", args.version, args.out),
+                 Release("macos-13",     "arm64", args.version, args.out),
+                 Release("ubuntu-22.04",   "x64", args.version, args.out),
                  Release("windows-2022",   "x64", args.version, args.out) ]
     if args.os:
         releases = list(filter(lambda release: release.os_name == args.os, releases))

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -297,7 +297,7 @@ protected virtual DfyParseFileResult ParseFile(DafnyOptions options, FileSnapsho
       filesContainer.Files.SelectMany(f => f.TopLevelDecls));
 
     return new DfyParseFileResult(null, uri,
-      filesContainer.Files.Where(f => !f.IsLibrary).Select(f => new Uri(f.Uri)).ToList(),
+      filesContainer.Files.Where(f => !f.IsLibrary).Select(f => DafnyFile.CreateCrossPlatformUri(f.Uri)).ToList(),
       new BatchErrorReporter(options), filesModule, syntaxDeserializer.SystemModuleModifiers);
   }
 

Source/DafnyCore/AST/SyntaxDeserializer/HandWritten.cs

@@ -93,7 +93,7 @@ public FilesContainer ReadFilesContainer() {
   public FileHeader ReadFileStart() {
     var uri = ReadString();
     var isLibrary = ReadBool();
-    this.uri = new Uri(uri);
+    this.uri = DafnyFile.CreateCrossPlatformUri(uri);
     var topLevelDecls = ReadList(ReadAbstract<TopLevelDecl>);
     return new FileHeader(uri, isLibrary, topLevelDecls);
   }

Source/DafnyCore/AST/Tokens.cs

@@ -82,6 +82,10 @@ public static string ToFileRangeString(this TokenRange? range, DafnyOptions opti
   }
 
   public static string GetRelativeFilename(DafnyOptions options, Token token) {
+    if (token.Uri == null) {
+      return token.Filepath ?? "unknown";
+    }
+
     var currentDirectory = Directory.GetCurrentDirectory();
     string filename = token.Uri.Scheme switch {
       "stdin" => "<stdin>",

Source/DafnyCore/DafnyFile.cs

@@ -7,6 +7,7 @@
 using System.Reflection;
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
+using System.Runtime.InteropServices;
 using System.Threading.Tasks;
 using DafnyAssembly;
 using DafnyCore;
@@ -320,4 +321,11 @@ public static List<string> FileNames(IReadOnlyList<DafnyFile> dafnyFiles) {
     return null;
   }
 
+  public static Uri CreateCrossPlatformUri(string path) {
+    // Only fixes Unix paths on Windows
+    if (RuntimeInformation.IsOSPlatform(OSPlatform.Windows) && path.StartsWith("/")) {
+      return new Uri("file://" + path);
+    }
+    return new Uri(path);
+  }
 }

Source/DafnyCore/JsonOutputWriter.cs

@@ -36,7 +36,7 @@ public Task Code(string message) {
   private Task WriteMessage(string message, string type) {
     return options.BaseOutputWriter.WriteLineAsync(new JsonObject() {
       ["type"] = type,
-      ["value"] = message
+      ["value"] = message.Replace("\r\n", "\n")
     }.ToJsonString());
   }
 
@@ -84,7 +84,7 @@ private static JsonObject SerializeToken(DafnyOptions options, TokenRange range)
     return new JsonObject {
       ["filename"] = range.StartToken.filename,
       ["filePath"] = TokenExtensions.GetRelativeFilename(options, range.StartToken),
-      ["uri"] = range.Uri!.AbsoluteUri,
+      ["uri"] = range.Uri?.AbsoluteUri ?? "file:///unknown",
       ["range"] = SerializeRange(range)
     };
   }

Source/DafnyCore/Options/ProjectFileOpener.cs

@@ -38,7 +38,14 @@ public ProjectFileOpener(IFileSystem fileSystem, IOrigin origin) {
   }
 
   protected virtual Task<DafnyProject?> OpenProjectInFolder(string folderPath) {
-    var configFileUri = new Uri(Path.Combine(folderPath, DafnyProject.FileName));
+    Uri configFileUri;
+    try {
+      configFileUri = new Uri(Path.Combine(folderPath, DafnyProject.FileName));
+    } catch (Exception) {
+      // On Windows systems, the URI "/Untitled-1" is not recognized for example
+      return Task.FromResult<DafnyProject?>(null);
+    }
+
     if (!fileSystem.Exists(configFileUri)) {
       return Task.FromResult<DafnyProject?>(null);
     }

Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg

@@ -222,7 +222,7 @@ solverRoots = os.pathsep.join(
 print(solverRoots)
 
 solverPath = \
-    lit.util.which("z3-4.8.5", solverRoots) or \
+    lit.util.which("z3-4.12.1", solverRoots) or \
     lit.util.which("cvc4", solverRoots)
 
 if not solverPath: