• feat: continue statements. Like Dafny's break statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section 19.2 of the Reference Manual. (#1839)
• feat: The keyword syntax for functions will change in Dafny version 4. The new command-line option /functionSyntax (see /help) allows early adoption of the new syntax. (#1832)
• feat: Attribute {:print} declares that a method may have print effects. Print effects are enforced only with /trackPrintEffects:1.
• feat: Add support for non-interactive solvers that need all SMT-Lib input in one batch (enabled with /proverOpt:BATCH_MODE=true). Inherited from Boogie 2.13 (boogie-org/boogie#512).
• fix: Allow /verificationLogger and /vcsCores to be usable together. Inherited from Boogie 2.13 (boogie-org/boogie#515).
• fix: Plug two memory leaks in Dafny's verification server. (#1858, #1863)
• fix: No warning "File contains no code" if a file only contains a submodule (#1840)
• fix: Stuck in verifying in VSCode - support for verification cancellation (#1771)
• fix: export-reveals of function-by-method now allows the function body to be ghost (#1855)
• fix: Regain C# 7.3 compatibility of the compiled code. (#1877)
• fix: The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion. (#1862)