From f629e447af0b88a710a394374254e0a82acb163d Mon Sep 17 00:00:00 2001 From: 0xb337r007 <0xe4e5@proton.me> Date: Thu, 22 Feb 2024 10:28:29 +0100 Subject: [PATCH] fix spec --- certora/specs/CollectibleV1.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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