Skip to content

Commit 8d4125f

Browse files
authored
Update ConstantProductPool.spec (#52)
1 parent e3237a7 commit 8d4125f

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -267,7 +267,7 @@ rule zeroWithdrawNoEffect(address to) {
267267
env e;
268268
setup(e);
269269
// The assumption is no skimming
270-
require currentContract.reserve1 == _token0.balanceOf(currentContract) && currentContract.reserve1 == _token1.balanceOf(currentContract);
270+
require currentContract.reserve0 == _token0.balanceOf(currentContract) && currentContract.reserve1 == _token1.balanceOf(currentContract);
271271
storage before = lastStorage;
272272
burnSingle(e, _token0, 0, to);
273273
storage after = lastStorage;

0 commit comments

Comments
 (0)