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
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
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