fix spec

status-im · Feb 22, 2024 · f629e44 · f629e44
1 parent 6a55d40
commit f629e44
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/certora/specs/CollectibleV1.spec b/certora/specs/CollectibleV1.spec
@@ -68,8 +68,8 @@ rule maxSupplyCannotBeLowerThanMintedCount() {
 }
 
 rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
-  require mintedCount() >= totalSupply();
   require maxSupply() >= totalSupply();
+  requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
 
   calldataarg args;
   f(e, args); // call all public/external functions of a contract