From 6a55d407cde0c573b5a6efee519935bfa85f3b16 Mon Sep 17 00:00:00 2001
From: 0xb337r007 <0xe4e5@proton.me>
Date: Thu, 22 Feb 2024 09:37:37 +0100
Subject: [PATCH] fix maxSupplyNotLowerThanTotalSupply in CollectibleV1 spec

---
 certora/specs/CollectibleV1.spec | 1 +
 1 file changed, 1 insertion(+)

diff --git a/certora/specs/CollectibleV1.spec b/certora/specs/CollectibleV1.spec
index 57e4c7f..6ff59d3 100644
--- a/certora/specs/CollectibleV1.spec
+++ b/certora/specs/CollectibleV1.spec
@@ -68,6 +68,7 @@ rule maxSupplyCannotBeLowerThanMintedCount() {
 }
 
 rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
+  require mintedCount() >= totalSupply();
   require maxSupply() >= totalSupply();
 
   calldataarg args;