diff --git a/src/Unicode/Utf8EncodingForm.dfy b/src/Unicode/Utf8EncodingForm.dfy
index 8a41129d..69a3a110 100644
--- 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
index 77bf42f3..ab4d73dc 100644
--- 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
   }
 }