contract/lib_openzeppelin_contracts/certora/specs/methods/IERC721Receiver.spec

methods {
  function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}