diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index 4983a40d6c6..220545e6422 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -567,8 +567,11 @@ void scheduleTCB(tcb_t *tptr)
 #ifdef CONFIG_KERNEL_MCS
 void postpone(sched_context_t *sc)
 {
-    tcbSchedDequeue(sc->scTcb);
-    tcbReleaseEnqueue(sc->scTcb);
+    tcb_t *tcb = sc->scTcb;
+    assert(tcb != NULL);
+
+    tcbSchedDequeue(tcb);
+    tcbReleaseEnqueue(tcb);
     NODE_STATE_ON_CORE(ksReprogram, sc->scCore) = true;
 }