From 09d5f07e0a754e79c2787e9b00b4712a74c9ea40 Mon Sep 17 00:00:00 2001
From: liav-certora <liav@certora.com>
Date: Wed, 24 Jan 2024 12:25:40 +0200
Subject: [PATCH] Update ConstantProductPool.spec

---
 DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec b/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec
index cd24e23f..8278e3c2 100644
--- a/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec
+++ b/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec
@@ -267,7 +267,7 @@ rule zeroWithdrawNoEffect(address to) {
     env e;
     setup(e);
     // The assumption is  no skimming 
-    require currentContract.reserve1 == _token0.balanceOf(currentContract) && currentContract.reserve1 == _token1.balanceOf(currentContract);
+    require currentContract.reserve0 == _token0.balanceOf(currentContract) && currentContract.reserve1 == _token1.balanceOf(currentContract);
     storage before = lastStorage;
     burnSingle(e, _token0, 0, to);
     storage after = lastStorage;