diff --git a/config.cmake b/config.cmake
index 4b8d0cec0c..bc6c0010a0 100644
--- a/config.cmake
+++ b/config.cmake
@@ -49,21 +49,15 @@ set_property(
 # These options are now set in seL4Config.cmake
 if(DEFINED CALLED_declare_default_headers)
     # calculate the irq cnode size based on MAX_NUM_IRQ
-    if("${KernelArch}" STREQUAL "riscv")
+    if(KernelArchRiscV)
         math(EXPR MAX_NUM_IRQ "${CONFIGURE_PLIC_MAX_NUM_INT} + 2")
-    else()
-        if(
-            DEFINED KernelMaxNumNodes
-            AND CONFIGURE_NUM_PPI GREATER "0"
-            AND "${KernelArch}" STREQUAL "arm"
+    elseif(KernelArchARM AND KernelEnableSMPSupport AND (CONFIGURE_NUM_PPI GREATER "0"))
+        math(
+            EXPR MAX_NUM_IRQ
+            "(${KernelMaxNumNodes}-1)*${CONFIGURE_NUM_PPI} + ${CONFIGURE_MAX_IRQ}"
         )
-            math(
-                EXPR MAX_NUM_IRQ
-                "(${KernelMaxNumNodes}-1)*${CONFIGURE_NUM_PPI} + ${CONFIGURE_MAX_IRQ}"
-            )
-        else()
-            set(MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ}")
-        endif()
+    else()
+        set(MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ}")
     endif()
     set(BITS "0")
     while(MAX_NUM_IRQ GREATER "0")