apalache-mc · konnov · May 20, 2022 · May 20, 2022 · May 20, 2022
diff --git a/.unreleased/breaking-changes/exit-codes.md b/.unreleased/breaking-changes/exit-codes.md
diff --git a/.unreleased/bug-fixes/non-det-pick.md b/.unreleased/bug-fixes/non-det-pick.md
diff --git a/.unreleased/bug-fixes/uinterpreted-types.md b/.unreleased/bug-fixes/uinterpreted-types.md
diff --git a/.unreleased/features/sound-records.md b/.unreleased/features/sound-records.md
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,3 +1,21 @@
+<!-- NOTE: This file is generated. Do not write release notes here.
+ Notes for unreleased changes go in the .unreleased/ directory. -->
+
+## 0.25.3 - 2022-05-20
+
+### Breaking changes
+
+- Introduce dedicated exit codes for type-checking errors, parser errors, and evaluation errors (e.g., due to unsupported language constructs or operators), see #1749
+
+### Features
+
+- Support sound records (over rows) in the model checker, see #1717
+
+### Bug fixes
+
+- Fix potential non-determinism when picking from `[S -> T]`, see #1753
+- Fix the bug in uninterpreted types, see #1792
+
 ## 0.25.2
 
 ### Features
@@ -852,4 +870,4 @@
 
 ## 0.3.0 [RELEASE]
 
- * the version presented at the TLA+ community meeting 2018 in Oxford
+ * the version presented at the TLA+ community meeting 2018 in Oxford
diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-0.25.3-SNAPSHOT
+0.25.4-SNAPSHOT