fixed rule description

3 years ago · 8c86b250bc
parent a0b58c3071
commit 8c86b250bc
1 changed files with 1 additions and 1 deletions
--- a/certora/specs/ERC20FlashMint.spec
+++ b/certora/specs/ERC20FlashMint.spec
@ -14,7 +14,7 @@ function specBurn(address account, uint256 amount) returns bool {   // retuns ne


 // STATUS - verified
-// fee + flashLoan amount is burned
+// Check that if flashLoan() call is successful, then proper amount of tokens was burnt(fee + flashLoan amount)
 rule letsWatchItBurns(env e){
    address receiver; address token; uint256 amount; bytes data;