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


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

Thank you