dafny-lang · MikaelMayer · Feb 6, 2025 · Feb 6, 2025
diff --git a/Snapshots.md b/Snapshots.md
@@ -7,6 +7,8 @@ layout: default
 
 - [Current development version](https://dafny.org/dafny)
 - [Latest release snapshot](https://dafny.org/latest)
+- [v4.10.0](https://dafny.org/v4.10.0)
+- [v4.9.1](https://dafny.org/v4.9.1)
 - [v4.8.1](https://dafny.org/v4.8.1)
 - [v4.6.0](https://dafny.org/v4.6.0)
 - [v4.5.0](https://dafny.org/v4.5.0)

diff --git a/latest/DafnyRef/Attributes.3.expect b/latest/DafnyRef/Attributes.3.expect
@@ -1,3 +1,3 @@
-text.dfy(25,14): Error: assertion might not hold
+text.dfy(25,6): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/Expressions.5.expect b/latest/DafnyRef/Expressions.5.expect
@@ -1,3 +1,3 @@
-text.dfy(2,11): Error: assertion might not hold
+text.dfy(2,2): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/Modules.2.expect b/latest/DafnyRef/Modules.2.expect
@@ -1,4 +1,4 @@
 text.dfy(9,6): Error: value does not satisfy the subset constraints of 'nat'
-text.dfy(12,21): Error: assertion might not hold
+text.dfy(12,4): Error: assertion might not hold
 
 Dafny program verifier finished with 1 verified, 2 errors
diff --git a/latest/DafnyRef/Modules.4.expect b/latest/DafnyRef/Modules.4.expect
@@ -1,3 +1,3 @@
-text.dfy(10,15): Error: assertion might not hold
+text.dfy(10,4): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/Plugins.md b/latest/DafnyRef/Plugins.md
@@ -230,6 +230,6 @@ That's it! Now, build your library while inside your folder:
 > dotnet build
 ```
 
-This will create the file `PluginTutorial/bin/Debug/net6.0/PluginTutorial.dll`.
+This will create the file `PluginTutorial/bin/Debug/net8.0/PluginTutorial.dll`.
 Now, open VSCode, open Dafny settings, and enter the absolute path to this DLL in the plugins section.
 Restart VSCode, and it should work!
diff --git a/latest/DafnyRef/Statements.10.expect b/latest/DafnyRef/Statements.10.expect
@@ -1,3 +1,3 @@
-text.dfy(8,13): Error: assertion might not hold
+text.dfy(8,4): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/Statements.16.expect b/latest/DafnyRef/Statements.16.expect
@@ -1,3 +1,3 @@
-text.dfy(17,10): Error: assertion might not hold
+text.dfy(17,2): Error: assertion might not hold
 
 Dafny program verifier finished with 2 verified, 1 error
diff --git a/latest/DafnyRef/Statements.3.expect b/latest/DafnyRef/Statements.3.expect
@@ -1,5 +1,5 @@
 text.dfy(12,2): Warning: this loop has no body (loop frame: i, a, $Heap)
-text.dfy(16,11): Error: assertion might not hold
-text.dfy(18,16): Error: assertion might not hold
+text.dfy(16,2): Error: assertion might not hold
+text.dfy(18,2): Error: assertion might not hold
 
 Dafny program verifier finished with 1 verified, 2 errors
diff --git a/latest/DafnyRef/Statements.5.expect b/latest/DafnyRef/Statements.5.expect
@@ -1,4 +1,4 @@
-text.dfy(2,14): Error: assertion might not hold
-text.dfy(3,11): Error: assertion might not hold
+text.dfy(2,2): Error: assertion might not hold
+text.dfy(3,2): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 2 errors
diff --git a/latest/DafnyRef/Statements.6.expect b/latest/DafnyRef/Statements.6.expect
@@ -1,3 +1,3 @@
-text.dfy(2,14): Error: assertion might not hold
+text.dfy(2,2): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/Statements.7.expect b/latest/DafnyRef/Statements.7.expect
@@ -1,3 +1,3 @@
-text.dfy(2,14): Error: assertion might not hold
+text.dfy(2,2): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/Statements.8b.expect b/latest/DafnyRef/Statements.8b.expect
@@ -1,4 +1,4 @@
-text.dfy(6,12): Error: function precondition could not be proved
+text.dfy(6,13): Error: function precondition could not be proved
 text.dfy(3,30): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 8 verified, 1 error
diff --git a/latest/DafnyRef/Statements.opaqueBlock.expect b/latest/DafnyRef/Statements.opaqueBlock.expect
@@ -1,3 +1,3 @@
-text.dfy(12,11): Error: assertion might not hold
+text.dfy(12,2): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/Topics.3.expect b/latest/DafnyRef/Topics.3.expect
@@ -1,3 +1,3 @@
 text.dfy(6,10): Error: the type of this variable is underspecified
-text.dfy(6,15): Error: type parameter 'T' (inferred to be '?') in the function call to 'EmptySet' could not be determined
+text.dfy(6,23): Error: type parameter 'T' (inferred to be '?') in the function call to 'EmptySet' could not be determined
 2 resolution/type errors detected in text.dfy
diff --git a/latest/DafnyRef/Types.19.expect b/latest/DafnyRef/Types.19.expect
@@ -1,3 +1,3 @@
-text.dfy(9,11): Error: assertion might not hold
+text.dfy(9,2): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/Types.20.expect b/latest/DafnyRef/Types.20.expect
@@ -1,5 +1,5 @@
 text.dfy(26,0): Error: a postcondition could not be proved on this return path
-text.dfy(25,10): Related location: this is the postcondition that could not be proved
+text.dfy(25,15): Related location: this is the postcondition that could not be proved
 text.dfy(10,9): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 1 verified, 1 error
diff --git a/latest/DafnyRef/Types.21.expect b/latest/DafnyRef/Types.21.expect
@@ -1,4 +1,4 @@
 text.dfy(8,4): Error: field 'x', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body
-text.dfy(10,13): Error: assertion might not hold
+text.dfy(10,4): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 2 errors
diff --git a/latest/DafnyRef/Types.25.expect b/latest/DafnyRef/Types.25.expect
@@ -1,3 +1,3 @@
-text.dfy(3,13): Error: assertion might not hold
+text.dfy(3,4): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/Types.7a.expect b/latest/DafnyRef/Types.7a.expect
@@ -1,3 +1,3 @@
-text.dfy(5,11): Error: assertion might not hold
+text.dfy(5,2): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/UserGuide.3.expect b/latest/DafnyRef/UserGuide.3.expect
@@ -1,3 +1,3 @@
-text.dfy(7,13): Error: assertion might not hold
+text.dfy(7,4): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/UserGuide.4.expect b/latest/DafnyRef/UserGuide.4.expect
@@ -1,3 +1,3 @@
-text.dfy(7,13): Error: assertion might not hold
+text.dfy(7,4): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/UserGuide.5.expect b/latest/DafnyRef/UserGuide.5.expect
@@ -1,3 +1,3 @@
-text.dfy(6,13): Error: assertion might not hold
+text.dfy(6,4): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/DafnyRef/UserGuide.md b/latest/DafnyRef/UserGuide.md
@@ -2732,7 +2732,7 @@ If you have Boogie installed locally, you can run the printed Boogie file with t
 DOTNET=$(which dotnet)
 
 BOOGIE_ROOT="path/to/boogie/Source"
-BOOGIE="$BOOGIE_ROOT/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll"
+BOOGIE="$BOOGIE_ROOT/BoogieDriver/bin/Debug/net8.0/BoogieDriver.dll"
 
 if [[ ! -x "$DOTNET" ]]; then
     echo "Error: Dafny requires .NET Core to run on non-Windows systems."
@@ -2769,7 +2769,7 @@ The following options are also commonly used:
   but a large positive number reports more errors per run
 
 * `--verification-time-limit:<n>` (was `-timeLimit:<n>`) - limits 
-  the number of seconds spent trying to verify each procedure.
+  the number of seconds spent trying to verify each assertion batch.
 
 
 ### 13.9.11. Controlling test generation {#sec-controlling-test-gen}

diff --git a/latest/DafnyRef/integration-java/IntegrationJava.md b/latest/DafnyRef/integration-java/IntegrationJava.md
@@ -218,3 +218,6 @@ Often this requires defining a Dafny class that corresponds to the Java class.
 the Dafny-generated (Java) types and the types used in the desired method.
 The wrapper will do appropriate conversions and call the desired method.
 
+## Performance notes
+
+If you have the choice, given a `m: map<K, V>`, prefer iterating over the map itself like `forall k <- m` rather than over the keys `forall k <- m.Keys`. The latter currently results in `O(N²)` steps, whereas the first one remains linear.
diff --git a/latest/HowToFAQ/Errors-Resolver2.md b/latest/HowToFAQ/Errors-Resolver2.md
@@ -168,7 +168,7 @@ and optimizing tail-recursion opportunities in mutually recursive functions.
 ```dafny
 function {:tailrecursion} f(n: nat): nat
 {
-  if n == 0 then n else var ff := f; ff(n-1)
+  if n == 0 then n else var r := f(n-1); r
 }
 ```
 

diff --git a/latest/Installation.md b/latest/Installation.md
@@ -15,7 +15,7 @@ are in the [Dafny project wiki](https://github.com/dafny-lang/dafny/wiki/INSTALL
 System Requirements
 ===================
 
-The `dafny tool` is a .NET 6.0 artifact, but it compiles to native executables on supported platforms.
+The `dafny tool` is a .NET 8.0 artifact, but it compiles to native executables on supported platforms.
 That and the Z3 tool are all that is needed to use dafny for verification; additional tools are 
 need for compilation, as described below.
 
@@ -41,7 +41,7 @@ In addition, the Dafny toolkit supplies runtime libraries, either in source form
 ### C#
 
 - Dafny targeting C# produces C#10-compatible source code.
-- Only the .NET 6.0 set of tools (which includes the C# compiler) is needed to compile and run the generated C# code.
+- Only the .NET 8.0 set of tools (which includes the C# compiler) is needed to compile and run the generated C# code.
 - The Dafny runtime library is included as C# source along with the generated C# code, so the user can compile those sources
 and any user code in one project.
 
@@ -86,9 +86,9 @@ For most users, we recommend using Dafny with VS Code, which has an easy install
 ## Visual Studio Code {#Visual-Studio-Code}
 
 0. Install [Visual Studio Code](https://code.visualstudio.com/)
-1. If you are on a Mac or Linux, install .NET 6.0, as described under those platforms below.  
+1. If you are on a Mac or Linux, install .NET 8.0, as described under those platforms below.
 2. In Visual Studio Code, press `Ctrl+P` (or `⌘P` on a Mac), and enter `ext install dafny-lang.ide-vscode`.
-3. If you open a `.dfy` file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions: 
+3. If you open a `.dfy` file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions:
   ![vs-code-dafny-2 0 1-install](https://user-images.githubusercontent.com/3601079/141353551-5cb5e23b-5536-47be-ba17-e5af494b775c.gif)
 
 ## Emacs {#Emacs}
@@ -118,7 +118,7 @@ install the correct dependencies for the desired language.
 
 To install Dafny on your own machine, 
 
-* Install (if not already present) .NET Core 6.0: `https://dotnet.microsoft.com/download/dotnet/6.0`
+* Install (if not already present) .NET Core 8.0: `https://dotnet.microsoft.com/download/dotnet/8.0`
 * Download the windows zip file from the [releases page](https://github.com/dafny-lang/dafny/releases/latest) and **save** it to your disk. 
 * Then, **before you open or unzip it**, right-click on it and select Properties; at the bottom of the dialog, click the **Unblock** button and then the OK button. 
 * Now, open the zip file and copy its contents into a directory on your machine. (You can now delete the zip file.)
@@ -130,7 +130,7 @@ Then:
 ## Linux (Binary) {#linux-binary}
 
 To install a binary installation of dafny on Linux (e.g., Ubuntu), do the following:
-* Install .NET 6.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-6.0`
+* Install .NET 8.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-8.0`
 * Install the Linux binary version of Dafny, from `https://github.com/dafny-lang/dafny/releases/latest`
 * Unzip the downloaded file in a (empty) location of your choice
 
@@ -165,7 +165,7 @@ After the compiler dependencies are installed, you can run a quick test of the i
 
 The .NET [NuGet](https://www.nuget.org/) repository collects .NET libraries and tools for easy installation. Dafny is available on NuGet, and can be installed as follows:
 
-* Install .NET 6.0 as described for your platform in one of the subsections above.
+* Install .NET 8.0 as described for your platform in one of the subsections above.
 * Install a binary version of Z3 4.12.1 for your platform from its [GitHub releases page](https://github.com/Z3Prover/z3/releases/tag/Z3-4.12.1) and put the `z3` executable in your `PATH`.
 * Install Dafny using `dotnet tool install --global dafny` (or leave out the `--global` to use with `dotnet tool run` from the source directory of a .NET project).
 
@@ -181,10 +181,10 @@ Additional instructions are found in the [Dafny User Guide](DafnyRef/DafnyRef#se
 
 ### C# (.Net)
 
-Install .NET 6.0:
-* Windows) `https://dotnet.microsoft.com/download/dotnet/6.0`
-* Linux) Install .NET 6.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-6.0`
-* Mac) Install .NET 6.0: `brew install dotnet-sdk` or from `https://docs.microsoft.com/dotnet/core/install/macos`
+Install .NET 8.0:
+* Windows) `https://dotnet.microsoft.com/download/dotnet/8.0`
+* Linux) Install .NET 8.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-8.0`
+* Mac) Install .NET 8.0: `brew install dotnet-sdk` or from `https://docs.microsoft.com/dotnet/core/install/macos`
 
 
 To separately compile and run your program for .NET:

diff --git a/latest/OnlineTutorial/Modules.1.expect b/latest/OnlineTutorial/Modules.1.expect
@@ -1,4 +1,4 @@
-text.dfy(27,23): Error: assertion might not hold
-text.dfy(37,23): Error: assertion might not hold
+text.dfy(27,4): Error: assertion might not hold
+text.dfy(37,4): Error: assertion might not hold
 
 Dafny program verifier finished with 5 verified, 2 errors
diff --git a/latest/OnlineTutorial/Modules.5.expect b/latest/OnlineTutorial/Modules.5.expect
@@ -1,3 +1,3 @@
-text.dfy(13,21): Error: assertion might not hold
+text.dfy(13,4): Error: assertion might not hold
 
 Dafny program verifier finished with 2 verified, 1 error
diff --git a/latest/OnlineTutorial/Sets.1.expect b/latest/OnlineTutorial/Sets.1.expect
@@ -1,3 +1,3 @@
-text.dfy(4,41): Error: assertion might not hold
+text.dfy(4,2): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/OnlineTutorial/guide.10.expect b/latest/OnlineTutorial/guide.10.expect
@@ -1,14 +1,14 @@
 text.dfy(7,0): Error: a postcondition could not be proved on this return path
+text.dfy(4,12): Related location: this is the postcondition that could not be proved
+text.dfy(7,0): Error: a postcondition could not be proved on this return path
 text.dfy(5,23): Related location: this is the postcondition that could not be proved
 text.dfy(7,0): Error: a postcondition could not be proved on this return path
 text.dfy(6,22): Related location: this is the postcondition that could not be proved
-text.dfy(7,0): Error: a postcondition could not be proved on this return path
-text.dfy(4,12): Related location: this is the postcondition that could not be proved
+text.dfy(16,0): Error: a postcondition could not be proved on this return path
+text.dfy(13,12): Related location: this is the postcondition that could not be proved
 text.dfy(16,0): Error: a postcondition could not be proved on this return path
 text.dfy(14,23): Related location: this is the postcondition that could not be proved
 text.dfy(16,0): Error: a postcondition could not be proved on this return path
 text.dfy(15,22): Related location: this is the postcondition that could not be proved
-text.dfy(16,0): Error: a postcondition could not be proved on this return path
-text.dfy(13,12): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 0 verified, 6 errors
diff --git a/latest/OnlineTutorial/guide.12.expect b/latest/OnlineTutorial/guide.12.expect
@@ -1,3 +1,3 @@
-text.dfy(9,11): Error: assertion might not hold
+text.dfy(9,2): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
diff --git a/latest/OnlineTutorial/guide.7.expect b/latest/OnlineTutorial/guide.7.expect
@@ -1,3 +1,3 @@
-text.dfy(14,11): Error: assertion might not hold
+text.dfy(14,2): Error: assertion might not hold
 
 Dafny program verifier finished with 1 verified, 1 error
diff --git a/latest/OnlineTutorial/guide.8.expect b/latest/OnlineTutorial/guide.8.expect
@@ -1,3 +1,3 @@
-text.dfy(11,11): Error: assertion might not hold
+text.dfy(11,2): Error: assertion might not hold
 
 Dafny program verifier finished with 1 verified, 1 error
diff --git a/latest/OnlineTutorial/guide.9.expect b/latest/OnlineTutorial/guide.9.expect
@@ -1,3 +1,3 @@
-text.dfy(10,11): Error: assertion might not hold
+text.dfy(10,2): Error: assertion might not hold
 
 Dafny program verifier finished with 1 verified, 1 error
diff --git a/latest/Snapshots.md b/latest/Snapshots.md
@@ -7,6 +7,8 @@ layout: default
 
 - [Current development version](https://dafny.org/dafny)
 - [Latest release snapshot](https://dafny.org/latest)
+- [v4.10.0](https://dafny.org/v4.10.0)
+- [v4.9.1](https://dafny.org/v4.9.1)
 - [v4.8.1](https://dafny.org/v4.8.1)
 - [v4.6.0](https://dafny.org/v4.6.0)
 - [v4.5.0](https://dafny.org/v4.5.0)

diff --git a/latest/VerificationOptimization/VerificationOptimization.md b/latest/VerificationOptimization/VerificationOptimization.md
@@ -608,6 +608,27 @@ As a general rule, designing a program from the start so that it can be broken i
 
 * Break methods up into smaller pieces, as well. Because methods are always opaque, this will, in many cases, require adding a contract to each broken-out method. To make this more tractable, consider abstracting the concepts used in those contracts into separate functions, some of which may be opaque.
 
+# Verification fine-tuning
+
+## Conjunction vs. Nested ifs
+
+We have witnessed cases where the following code:
+```dafny
+    if (a && b) {
+        assert true;
+    }
+```
+verifies slower than
+```dafny
+    if (a) {
+        if (b) {
+            assert true;
+        }
+    }
+```
+This is because the well-formedness of `&& b` adds an extra proof obligation, which is empty in this case but not trimmed, so there is an extra `if (a) {}` in the encoding.
+Therefore, for verification performance, the nested ifs _could_ verify faster, and we have witnessed one case where it does. In other cases, this difference in translation might trigger butterfly effects and uncover brittleness.
+
 # Summary
 
 When you're dealing with a program that exhibits high verification variability, or simply slow or unsuccessful verification, careful encapsulation and information hiding combined with hints to add information in the context of difficult constructs is frequently the best solution. Breaking one large definition with extensive contracts down into several, smaller definitions, each with simpler contracts, can be very valuable. Within each smaller definition, a few internal, locally-encapsulated hints can help the prover make effective progress on goals it might be unable to prove in conjunction with other code.

diff --git a/latest/index.html b/latest/index.html
@@ -31,6 +31,7 @@ <h2>Quick Links</h2>
 <ul>
 <li><a href="./Installation"><b>Installation</b></a>
      (or a <a href="https://marketplace.visualstudio.com/items?itemName=dafny-lang.ide-vscode">VSCode plugin for Dafny</a>)</li>
+<li><a href="https://dafny.zulipchat.com/" target="_blank" rel="noopener noreferrer">Zulip channel</a> to ask questions about Dafny</li>
 <li><a href="./DafnyRef/DafnyRef">Dafny Reference Manual and User Guide</a></li>
 <li><a href="./toc">Dafny Resources for Users</a></li>
 <li><a href="https://github.com/dafny-lang/dafny">Dafny GitHub project (for developers of the Dafny tools themselves)</a></li>

diff --git a/latest/news/6006.fix b/latest/news/6006.fix
@@ -0,0 +1 @@
+Fix soundness bug that could occur for opaque blocks with empty modifies clauses
diff --git a/latest/news/6028.feat b/latest/news/6028.feat
@@ -0,0 +1 @@
+Change the default value for --verification-time-limit to 30 seconds instead of 0 (no limit)
diff --git a/latest/news/fix.3809 b/latest/news/fix.3809
@@ -0,0 +1 @@
+Fix C#, Java and Go generated code when a datatype contains a method named 'Default'
diff --git a/latest/news/fix.5746 b/latest/news/fix.5746
@@ -0,0 +1 @@
+Fix C# generated code when a module contains a type with the same name
diff --git a/latest/news/fix.6014 b/latest/news/fix.6014
@@ -0,0 +1 @@
+Fix Java generated code when a module contains a type with the same name
diff --git a/v4.10.0/.gitignore b/v4.10.0/.gitignore
@@ -0,0 +1,7 @@
+**/.DS_Store
+_site
+.sass-cache
+.jekyll-cache
+.jekyll-metadata
+vendor
+DafnyRefZ.md
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Fix soundness bug that could occur for opaque blocks with empty modifies clauses
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Change the default value for --verification-time-limit to 30 seconds instead of 0 (no limit)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Fix C#, Java and Go generated code when a datatype contains a method named 'Default'
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Fix C# generated code when a module contains a type with the same name
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Fix Java generated code when a module contains a type with the same name