# CONFIG_MAXSMP is not set