add missing invariant
This commit is contained in:
parent
9194946d1d
commit
e7333a350e
|
@ -69,6 +69,7 @@ rule maxSupplyCannotBeLowerThanMintedCount() {
|
||||||
|
|
||||||
rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
|
rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
|
||||||
require maxSupply() >= totalSupply();
|
require maxSupply() >= totalSupply();
|
||||||
|
requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
|
||||||
|
|
||||||
calldataarg args;
|
calldataarg args;
|
||||||
f(e, args); // call all public/external functions of a contract
|
f(e, args); // call all public/external functions of a contract
|
||||||
|
|
Loading…
Reference in New Issue