@@ -20,7 +20,7 @@ methods {
20
20
// external calls to StrategyManager
21
21
function _ . getDeposits ( address ) external => DISPATCHER ( true ) ;
22
22
function _ . slasher ( ) external => DISPATCHER ( true ) ;
23
- function _ . addShares ( address , address , uint256 ) external => DISPATCHER ( true ) ;
23
+ function _ . addShares ( address , address , address , uint256 ) external => DISPATCHER ( true ) ;
24
24
function _ . removeShares ( address , address , uint256 ) external => DISPATCHER ( true ) ;
25
25
function _ . withdrawSharesAsTokens ( address , address , uint256 , address ) external => DISPATCHER ( true ) ;
26
26
@@ -97,7 +97,7 @@ definition methodCanIncreaseShares(method f) returns bool =
97
97
f . selector == sig :depositIntoStrategy ( address , address , uint256 ) . selector
98
98
|| f . selector == sig :depositIntoStrategyWithSignature ( address , address , uint256 , address , uint256 , bytes ) . selector
99
99
|| f . selector == sig :withdrawSharesAsTokens ( address , address , uint256 , address ) . selector
100
- || f . selector == sig :addShares ( address , address , uint256 ) . selector ;
100
+ || f . selector == sig :addShares ( address , address , address , uint256 ) . selector ;
101
101
102
102
/**
103
103
* a staker's amount of shares in a strategy (i.e. `stakerStrategyShares[staker][strategy]`) should only decrease when
@@ -129,7 +129,7 @@ rule newSharesIncreaseTotalShares(address strategy) {
129
129
uint256 stakerStrategySharesBefore = get_stakerStrategyShares ( e . msg . sender , strategy ) ;
130
130
uint256 totalSharesBefore = totalShares ( strategy ) ;
131
131
if (
132
- f . selector == sig :addShares ( address , address , uint256 ) . selector
132
+ f . selector == sig :addShares ( address , address , address , uint256 ) . selector
133
133
|| f . selector == sig :removeShares ( address , address , uint256 ) . selector
134
134
) {
135
135
uint256 totalSharesAfter = totalShares ( strategy ) ;
0 commit comments