m

ajewellamz · ajewellamz · commit d622567d0b56 · 2025-07-25T15:28:26.000-04:00
diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -242,7 +242,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       ensures client.ValidState()
       modifies client.Modifies
     {
-      var counts: array<int> := new int[100];
+      var counts: array<int> := new int[100](i => 0);
       for i := 0 to numBuckets {
         DoBucketQuery(client, i, q, counts, queryName, custom, numBuckets);
       }

Original file line number	Diff line number	Diff line change
`@@ -242,7 +242,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {`
`242`	`242`	`ensures client.ValidState()`
`243`	`243`	`modifies client.Modifies`
`244`	`244`	`{`
`245`		`- var counts: array<int> := new int[100];`
	`245`	`+ var counts: array<int> := new int[100](i => 0);`
`246`	`246`	`for i := 0 to numBuckets {`
`247`	`247`	`DoBucketQuery(client, i, q, counts, queryName, custom, numBuckets);`
`248`	`248`	`}`