diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy
index e2c4036f7..e841deb98 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy
@@ -47,9 +47,11 @@ module DdbMiddlewareConfig {
   function SearchModifies(config: Config) : set<object>
   {
     //set x, y | y in config.tableEncryptionConfigs && x in OneSearchModifies(config.tableEncryptionConfigs[y]) :: x
-    set versions <- set configValue <- config.tableEncryptionConfigs.Values | configValue.search.Some? :: configValue.search.value.versions,
-      keyStore <- set version <- versions :: version.keySource.store,
-      obj <- keyStore.Modifies | obj in keyStore.Modifies :: obj
+    set
+      versions <- (set configValue <- config.tableEncryptionConfigs.Values | configValue.search.Some? :: configValue.search.value.versions),
+      keyStore <- (set version <- versions :: version.keySource.store),
+      obj <- keyStore.Modifies
+             {:nowarn} :: obj
 
   }
 
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
index 77f3b7aab..56ba4ea1f 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
@@ -132,7 +132,7 @@ module
              + (if tableConfig.legacyOverride.Some? then tableConfig.legacyOverride.value.encryptor.Modifies else {})
              + (if tableConfig.search.Some? then tableConfig.search.value.versions[0].keyStore.Modifies else {})
            )
-      :: o;
+           {:nowarn} :: o; // ignore warning for missing trigger on quantifier
 
     var allLogicalTableNames := {};
     var i := 0;
diff --git a/SharedMakefile.mk b/SharedMakefile.mk
index 37f18d5f6..06e523004 100644
--- a/SharedMakefile.mk
+++ b/SharedMakefile.mk
@@ -13,9 +13,9 @@ include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
 
 VERIFY_TIMEOUT := 250
 
-verify:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
-verify_single:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
-verify_service:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
+verify:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts --log-format csv
+verify_single:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts --log-format csv
+verify_service:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts --log-format csv
 
 transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-module-names --allow-external-contracts
 transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-module-names --allow-external-contracts