debug 4.4 upgrade

smithy-lang · Dec 15, 2023 · c38c480 · c38c480
1 parent 11c1461
commit c38c480
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy b/TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy
@@ -190,6 +190,7 @@ module {:extern "UTF8"} UTF8 {
       invariant lo <= |s|
       invariant ValidUTF8Range(s, lo, |s|)
       invariant ValidUTF8Range(s + t, 0, |s + t|) == ValidUTF8Range(s + t, lo, |s + t|)
+      decreases |s| - lo
     {
       var r := (s + t)[lo..];
       if Uses1Byte(r) {