diff --git a/AwsCryptographyPrimitives/test/TestECDH.dfy b/AwsCryptographyPrimitives/test/TestECDH.dfy
index f3935caf9..aead61423 100644
--- a/AwsCryptographyPrimitives/test/TestECDH.dfy
+++ b/AwsCryptographyPrimitives/test/TestECDH.dfy
@@ -458,7 +458,7 @@ module TestECDH {
     }
   }
 
-  method {:test} TestCompressDecompressConstantPublicKeys() {
+  method {:test} {:vcs_split_on_every_assert} TestCompressDecompressConstantPublicKeys() {
     var derX509PublicKeys := [ECC_P256_PUBLIC, ECC_384_PUBLIC, ECC_P521_PUBLIC];
     var compressedKeys := [ECC_P256_PUBLIC_COMPRESSED, ECC_384_PUBLIC_COMPRESSED, ECC_P521_PUBLIC_COMPRESSED];
     var curves := [P256, P384, P521];
diff --git a/project.properties b/project.properties
index 0a1c10360..255f8ddc0 100644
--- a/project.properties
+++ b/project.properties
@@ -6,5 +6,5 @@
 # The Java project include this file as a Gradle properties
 # And the Dotnet projects include and parse this file.
 dafnyVersion=4.2.0
-dafnyVerifyVersion=4.2.0
+dafnyVerifyVersion=4.7.0
 mplVersion=1.5.1-SNAPSHOT
diff --git a/smithy-dafny b/smithy-dafny
index 2baebfbcb..a0fd2c595 160000
--- a/smithy-dafny
+++ b/smithy-dafny
@@ -1 +1 @@
-Subproject commit 2baebfbcb4b62ed0949c185610316725019a6dae
+Subproject commit a0fd2c595fe7d16f0a18a7bbdcb056bdcb695192