Remove try/catch block around vault.deposit from function verify_depositProperties.
The previous implementation seemed to be a work-in-progress piece of code left out in this contract, as the logic is different from the other functions: verify_mintProperties, verify_redeemProperties, and verify_withdrawProperties.
Moreover, the previous implementation would prevent echidna from successfully completing when deposits reverted due to an invalid parameter. For example, in case an ERC4264 vault requires a minimum deposit amount. This might be the case when the vault tries to address the issue H-01 Vault deposits can be front-run and user funds stolen from OpenZeppelin ERC4626 Tokenized Vault Audit by reverting when assets is zero.
Remove
try/catch
block aroundvault.deposit
from functionverify_depositProperties
.The previous implementation seemed to be a work-in-progress piece of code left out in this contract, as the logic is different from the other functions:
verify_mintProperties
,verify_redeemProperties
, andverify_withdrawProperties
.Moreover, the previous implementation would prevent echidna from successfully completing when deposits reverted due to an invalid parameter. For example, in case an ERC4264 vault requires a minimum deposit amount. This might be the case when the vault tries to address the issue
H-01 Vault deposits can be front-run and user funds stolen
from OpenZeppelin ERC4626 Tokenized Vault Audit by reverting whenassets
is zero.