# CONFIG_X86_VSMP is not set