How to avoid Certora havocking on payable.transfer function


Hi, I am verifying a function using Certora and in that function there is a line

payable(msg.sender).transfer(ethBal)

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 address.call{value: 0}(data)?

Thank you