Chore: Fix verification for 4.9

This change, although unexpected, is required to make verification of the libraries to pass for 4.9
dafny-lang · Oct 30, 2024 · 07e89fb · 07e89fb
1 parent fabf44d
commit 07e89fb
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/src/Unicode/Utf8EncodingForm.dfy b/src/Unicode/Utf8EncodingForm.dfy
@@ -251,6 +251,8 @@ module {:options "-functionSyntax:4"} Utf8EncodingForm refines UnicodeEncodingFo
     var y := (thirdByte & 0x3F) as bv24;
     var x := (fourthByte & 0x3F) as bv24;
     assert {:split_here} true;
-    (u1 << 18) | (u2 << 16) | (z << 12) | (y << 6) | x as Unicode.ScalarValue
+    var v := (u1 << 18) | (u2 << 16) | (z << 12) | (y << 6) | x as Unicode.ScalarValue;
+    assert EncodeScalarValueQuadrupleByte(v) == m;
+    v
   }
 }
diff --git a/src/dafny/Unicode/Utf8EncodingForm.dfy b/src/dafny/Unicode/Utf8EncodingForm.dfy
@@ -251,6 +251,8 @@ module {:options "-functionSyntax:4"} Dafny.Utf8EncodingForm refines UnicodeEnco
     var y := (thirdByte & 0x3F) as bv24;
     var x := (fourthByte & 0x3F) as bv24;
     assert {:split_here} true;
-    (u1 << 18) | (u2 << 16) | (z << 12) | (y << 6) | x as Unicode.ScalarValue
+    var v := (u1 << 18) | (u2 << 16) | (z << 12) | (y << 6) | x as Unicode.ScalarValue;
+    assert EncodeScalarValueQuadrupleByte(v) == m;
+    v
   }
 }