diff --git a/libsel4vm/src/arch/arm/boot.c b/libsel4vm/src/arch/arm/boot.c
index f50010e63..772e3293e 100644
--- a/libsel4vm/src/arch/arm/boot.c
+++ b/libsel4vm/src/arch/arm/boot.c
@@ -111,11 +111,5 @@ int vm_create_vcpu_arch(vm_t *vm, vm_vcpu_t *vcpu)
     }
 #endif /* CONFIG_MAX_NUM_NODES > 1 */
 
-#ifdef CONFIG_DEBUG_BUILD
-    char vcpu_name[32];
-    snprintf(vcpu_name, sizeof(vcpu_name), "%s:%d", vm->vm_name, vcpu->vcpu_id);
-    seL4_DebugNameThread(vm_get_vcpu_tcb(vcpu), vcpu_name);
-#endif
-
     return err;
 }
diff --git a/libsel4vm/src/boot.c b/libsel4vm/src/boot.c
index 656ef9a8b..92fe00f4b 100644
--- a/libsel4vm/src/boot.c
+++ b/libsel4vm/src/boot.c
@@ -76,6 +76,11 @@ vm_vcpu_t *vm_create_vcpu(vm_t *vm, int priority)
     vcpu_new->target_cpu = -1;
     err = vm_create_vcpu_arch(vm, vcpu_new);
     assert(!err);
+#ifdef CONFIG_DEBUG_BUILD
+    char vcpu_name[32];
+    snprintf(vcpu_name, sizeof(vcpu_name), "%s:%d", vm->vm_name, vcpu_new->vcpu_id);
+    seL4_DebugNameThread(vm_get_vcpu_tcb(vcpu_new), vcpu_name);
+#endif
     vm->vcpus[vm->num_vcpus] = vcpu_new;
     vm->num_vcpus++;
     return vcpu_new;