From bc0f996ee18367ae10211f0634bf9ff841794979 Mon Sep 17 00:00:00 2001
From: John Tristan <trjohnb@amazon.com>
Date: Thu, 2 Mar 2023 09:44:52 -0500
Subject: [PATCH] Release Dafny 3.13.0

---
 RELEASE_NOTES.md             | 17 +++++++++++++++++
 Source/Directory.Build.props |  2 +-
 docs/dev/news/2266.fix       |  1 -
 docs/dev/news/3479.fix       |  1 -
 docs/dev/news/3641.feat      |  1 -
 docs/dev/news/3641.fix       |  3 ---
 6 files changed, 18 insertions(+), 7 deletions(-)
 delete mode 100644 docs/dev/news/2266.fix
 delete mode 100644 docs/dev/news/3479.fix
 delete mode 100644 docs/dev/news/3641.feat
 delete mode 100644 docs/dev/news/3641.fix

diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 29c8493cbc1..29c86a6c2d2 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -2,6 +2,23 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 3.13.0
+
+## New features
+
+- Expose non-relaxed definite assignment (`/definiteAssignment:4`) in legacy CLI (https://github.com/dafny-lang/dafny/pull/3641)
+
+## Bug fixes
+
+- Fix translation of Dafny FunctionHandles to Boogie (https://github.com/dafny-lang/dafny/pull/2266)
+
+- To ensure that a `class` correctly implements a `trait`, we perform an override check. This check was previously faulty across `module`s, but works unconditionally now. (https://github.com/dafny-lang/dafny/pull/3479)
+
+- Fixes to definite assignment and determinism options:
+     - `--enforce-determinism` now forbids constructor-less classes
+     - With non-relaxed definite assignment, allow auto-init fields to be uninitialized
+  (https://github.com/dafny-lang/dafny/pull/3641)
+
 # 3.12.0
 
 ## New features
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index 8b31d0da3b7..ece6e185efd 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -1,7 +1,7 @@
 <Project>
 
   <PropertyGroup>
-    <VersionPrefix>3.12.0.50221<!--Version 3.12.0, year 2018+5, month 2, day 21.--></VersionPrefix>
+    <VersionPrefix>3.13.0.50302<!--Version 3.13.0, year 2018+5, month 3, day 2.--></VersionPrefix>
     <NoWarn>1701;1702;VSTHRD200</NoWarn>
   </PropertyGroup>
  
diff --git a/docs/dev/news/2266.fix b/docs/dev/news/2266.fix
deleted file mode 100644
index 4af9dd8f5e3..00000000000
--- a/docs/dev/news/2266.fix
+++ /dev/null
@@ -1 +0,0 @@
-Fix translation of Dafny FunctionHandles to Boogie
diff --git a/docs/dev/news/3479.fix b/docs/dev/news/3479.fix
deleted file mode 100644
index 96e3176bae2..00000000000
--- a/docs/dev/news/3479.fix
+++ /dev/null
@@ -1 +0,0 @@
-To ensure that a `class` correctly implements a `trait`, we perform an override check. This check was previously faulty across `module`s, but works unconditionally now.
diff --git a/docs/dev/news/3641.feat b/docs/dev/news/3641.feat
deleted file mode 100644
index 19b2576ed7e..00000000000
--- a/docs/dev/news/3641.feat
+++ /dev/null
@@ -1 +0,0 @@
-Expose non-relaxed definite assignment (`/definiteAssignment:4`) in legacy CLI
\ No newline at end of file
diff --git a/docs/dev/news/3641.fix b/docs/dev/news/3641.fix
deleted file mode 100644
index b4364957e12..00000000000
--- a/docs/dev/news/3641.fix
+++ /dev/null
@@ -1,3 +0,0 @@
-Fixes to definite assignment and determinism options:
-   - `--enforce-determinism` now forbids constructor-less classes
-   - With non-relaxed definite assignment, allow auto-init fields to be uninitialized