diff --git a/certora/specs/CollectibleV1.spec b/certora/specs/CollectibleV1.spec index 6ff59d3..986182b 100644 --- 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