From a0b58c30710910cc805d10d0cf20ebf2c99ff7f6 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Mon, 4 Apr 2022 21:16:15 +0100
Subject: [PATCH] flashMint finished

---
 certora/specs/ERC20FlashMint.spec | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec
index 511eaf84f..eb605893b 100644
--- a/certora/specs/ERC20FlashMint.spec
+++ b/certora/specs/ERC20FlashMint.spec
@@ -1,9 +1,8 @@
 import "erc20.spec"
 
 methods {
-    onFlashLoan(address, address, uint256, uint256, bytes) => HAVOC_ALL
-
-    _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount);
+    maxFlashLoan(address) returns(uint256) envfree
+    _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount)
 }
 
 ghost mapping(address => uint256) trackedBurnAmount;
@@ -26,4 +25,4 @@ rule letsWatchItBurns(env e){
     uint256 burned = trackedBurnAmount[receiver];
 
     assert to_mathint(amount + feeBefore) == burned, "cheater";
-}
\ No newline at end of file
+}