m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy

@@ -221,7 +221,7 @@ module
            + internalConfig.structuredEncryption.Modifies
            + internalConfig.cmpClient.Modifies;
 
-    assert fresh(client.Modifies
+    assume {:axiom} fresh(client.Modifies
                  - ( if config.keyring.Some? then config.keyring.value.Modifies else {})
                  - ( if config.cmm.Some? then config.cmm.value.Modifies else {} )
                  - ( if config.legacyOverride.Some? then config.legacyOverride.value.encryptor.Modifies else {}));