From c3b002182626ee6e0ccf123a1ad92a07b8146eb7 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 26 Jan 2024 16:45:05 -0800 Subject: [PATCH] Embellish release notes of PR 4928 (#5016) Embellish release notes of PR #4928. The release note now try to make it clear that any new errors (for this issue) on previous programs are intentional. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- docs/dev/news/4928.fix | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/dev/news/4928.fix b/docs/dev/news/4928.fix index 4f1d3d2b04..cea1c2572b 100644 --- a/docs/dev/news/4928.fix +++ b/docs/dev/news/4928.fix @@ -1 +1,3 @@ -Check for correct usage of type characteristics in specifications and other places where they were missing +Check for correct usage of type characteristics in specifications and other places where they were missing. + +This fix will cause build breaks for programs with missing type characteristics (like `(!new)` and `(0)`). Any such error message is accompanied with a hint about what type characterics need to be added where.