fix spec
This commit is contained in:
parent
6a55d407cd
commit
f629e447af
|
@ -68,8 +68,8 @@ rule maxSupplyCannotBeLowerThanMintedCount() {
|
||||||
}
|
}
|
||||||
|
|
||||||
rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
|
rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
|
||||||
require mintedCount() >= totalSupply();
|
|
||||||
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