Error while testing custom spec for ERC20

Exception message: No lastStorage in storage var families: {}
[main] ERROR ALWAYS - Encountered exception Certora internal exception; please report this to Certora.

Insights link

thanks for reporting this, it looks like it is due a parametric function call with parameters:
f(e, spender, amount);
Note that parametric method calls can only take single calldataarg argument

Gotcha… I was hoping to avoid using function selectors one by one since multiple functions have signature f(address, uint256). Is there a way to do this without specifying each function selector individually?

Currently there is no way to do that, if it is needed in many rules we suggest to have a in the spec a function that calls the different methods with the right arguments. sushiswap/MasterChefV2.spec at 56cedd0e06a6cf665083b3a662f9f77b80303ebe · sushiswap/sushiswap · GitHub