diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
index 7ead82092..311480236 100644
--- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
+++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
@@ -880,9 +880,7 @@ LIBSEL4_INLINE_FUNC seL4_Word seL4_DebugGetThreadAffinity(seL4_CPtr tcb)
 {
     seL4_Word unused0 = 0;
     seL4_Word unused1 = 0;
-    seL4_Word unused2 = 0;
-    seL4_Word unused3 = 0;
-    seL4_Word unused4 = 0;
+    LIBSEL4_UNUSED seL4_Word unused2 = 0;
 
     seL4_Word affinity = 0;
 
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
index fda4aa161..07968d418 100644
--- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
@@ -686,7 +686,7 @@ LIBSEL4_INLINE_FUNC seL4_Word seL4_DebugGetThreadAffinity(seL4_CPtr tcb)
     seL4_Word affinity = 0;
 
     x64_sys_send_recv(seL4_SysDebugGetThreadAffinity, tcb, &affinity, 0,
-                      &unused0, &unused1, &unused3, &unused4, &unused5, 0);
+                      &unused0, &unused1, &unused2, &unused3, &unused4, 0);
     return affinity;
 }
 #endif /* CONFIG_ENABLE_SMP_SUPPORT */