Hi, I am verifying a function using Certora and in that function there is a line
It looks Certora doesn’t know how to execute that (which is surprising since this is a built-in function on payable type), hence it havocked the call.
Given the transfer is a built-in function on payable. How can we avoid the havocking?
A related question is if it’s possible to prevent Certora havocking on