Is there a good reason to use multiple env variables in my rule instead of one?
env variables hold transaction and block properties (for example msg.sender, block.timestamp). If your rule checks things regarding this type of information you will probably have to use different env variables, otherwise you will have much less coverage or even get vacuous results.
For example, say I want to check some properties of foo(), which has an onlyOwner modifier followed by execution of bar(). If bar() access msg.sender, it will always be the owner.
For further information about env variables, take a look at https://docs.certora.com/en/latest/docs/ref-manual/cvl/types.html#the-env-type
1 Like