# CONFIG_HCALL_STATS is not set