diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
index 3b68d6df7..a72e05137 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
@@ -653,7 +653,7 @@ module MessageBody {
     return Success(finalFrame);
   }
 
-  method DecryptFramedMessageBody(
+  method {:vcs_split_on_every_assert} DecryptFramedMessageBody(
     body: FramedMessage,
     key: seq<uint8>,
     crypto: Primitives.AtomicPrimitivesClient
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy
index a02093229..cba5fc977 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy
@@ -263,7 +263,7 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys {
     }
   }
 
-  lemma ReadEncryptedDataKeysSectionIsComplete(
+  lemma {:vcs_split_on_every_assert} ReadEncryptedDataKeysSectionIsComplete(
     data: ESDKEncryptedDataKeys,
     bytes: seq<uint8>,
     buffer: ReadableBuffer,