diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml
index 6f310c42d..7dc7fa627 100644
--- a/.github/workflows/ci_test_vector_java.yml
+++ b/.github/workflows/ci_test_vector_java.yml
@@ -32,12 +32,17 @@ jobs:
         os: [
             # Run on ubuntu image that comes pre-configured with docker
             ubuntu-22.04,
+            macos-13,
           ]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
       contents: read
     steps:
+      - name: Setup Docker
+        if: matrix.os == 'macos-13' && matrix.library == 'TestVectors'
+        uses: douglascamata/setup-docker-macos-action@v1.0.0
+
       - name: Setup DynamoDB Local
         uses: rrainn/dynamodb-action@v4.0.0
         with:
diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml
index b05e4dbd5..46ec60bf5 100644
--- a/.github/workflows/ci_test_vector_net.yml
+++ b/.github/workflows/ci_test_vector_net.yml
@@ -28,12 +28,17 @@ jobs:
         os: [
             # Run on ubuntu image that comes pre-configured with docker
             ubuntu-22.04,
+            macos-13,
           ]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
       contents: read
     steps:
+      - name: Setup Docker
+        if: matrix.os == 'macos-13' && matrix.library == 'TestVectors'
+        uses: douglascamata/setup-docker-macos-action@v1.0.0
+
       - name: Setup DynamoDB Local
         uses: rrainn/dynamodb-action@v4.0.0
         with:
diff --git a/.github/workflows/library_rust_tests.yml b/.github/workflows/library_rust_tests.yml
index 987a6946a..a6167f536 100644
--- a/.github/workflows/library_rust_tests.yml
+++ b/.github/workflows/library_rust_tests.yml
@@ -36,7 +36,7 @@ jobs:
     steps:
       - name: Setup Docker
         if: matrix.os == 'macos-13' && matrix.library == 'TestVectors'
-        uses: douglascamata/setup-docker-macos-action@v1-alpha
+        uses: douglascamata/setup-docker-macos-action@v1.0.0
 
       - name: Setup DynamoDB Local
         if: matrix.library == 'TestVectors'
diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index ba6588ca5..8ed52309d 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -665,13 +665,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         results[i] := FullSearch(client, queries[i]);
       }
 
-      var configs := tableEncryptionConfigs.Keys;
-      while configs != {}
-        decreases |configs|
-        invariant forall k <- configs :: k in tableEncryptionConfigs
+      var configs := SortedSets.ComputeSetToOrderedSequence2(tableEncryptionConfigs.Keys, CharLess);
+      for i := 0 to |configs|
       {
-        var config :| config in configs;
-        configs := configs - { config };
+        var config := configs[i];
         BasicQueryTestConfig(tableEncryptionConfigs[config], results, globalRecords);
       }
     }