diff --git a/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
index 3111d22c9..10a8a1926 100644
--- a/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
@@ -171,7 +171,7 @@ typedef enum {
 #define seL4_HugePageBits 30
 #define seL4_SlotBits 5
 #if defined(CONFIG_HARDWARE_DEBUG_API) || defined(CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE) || \
-    (defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined(CONFIG_ENABLE_SMP_SUPPORT) && defined(CONFIG_BENCHMARK_TRACK_UTILISATION))
+    (defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined(CONFIG_ENABLE_SMP_SUPPORT) && defined(CONFIG_BENCHMARK_TRACK_UTILISATION) && !defined(CONFIG_KERNEL_MCS))
 #define seL4_TCBBits 12
 #else
 #define seL4_TCBBits 11