diff --git a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy index 64fd2441e..32b45ef0c 100644 --- a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy +++ b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy @@ -46,6 +46,7 @@ module {:options "/functionSyntax:4"} AllEsdkV4NoReqEc { const AllPositiveKeyringTestsNoReqCmmNoKmsRsa := {} + + AllDefaultCmm.SuccessTestingRequiredEncryptionContextKeysReproducedEncryptionContext + AllHierarchy.Tests + AllKms.Tests + AllKmsMrkAware.Tests diff --git a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy index beacc23b6..c74b1b460 100644 --- a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy +++ b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy @@ -34,7 +34,7 @@ module {:options "/functionSyntax:4" } AllEsdkV4WithReqEc { const AllPositiveReqEcTests := AllRequiredEncryptionContextCmm.SuccessTestingRequiredEncryptionContextKeysReproducedEncryptionContext // These are only required encryption context vectors with static aes keyrings - const AllPositveReqEcEsdkTests := + const AllPositiveReqEcEsdkTests := set config <- AllPositiveReqEcTests, algorithmSuite <- @@ -55,5 +55,5 @@ module {:options "/functionSyntax:4" } AllEsdkV4WithReqEc { ) const Tests := - AllPositveReqEcEsdkTests + AllPositiveReqEcEsdkTests } \ No newline at end of file