diff -ur xenomai-2.5.5.2/include/nucleus/sched.h xenomai-2.5.5.2.new/include/nucleus/sched.h
--- xenomai-2.5.5.2/include/nucleus/sched.h	2010-10-03 14:35:17.000000000 +0200
+++ xenomai-2.5.5.2.new/include/nucleus/sched.h	2010-11-04 15:58:48.000000000 +0100
@@ -185,7 +185,6 @@
   setbits(current_sched->status, XNRESCHED);				\
   if (current_sched != (__sched__))	{				\
       xnarch_cpu_set(xnsched_cpu(__sched__), current_sched->resched);	\
-      setbits((__sched__)->status, XNRESCHED);				\
   }									\
 } while (0)
 
diff -ur xenomai-2.5.5.2/ksrc/nucleus/pod.c xenomai-2.5.5.2.new/ksrc/nucleus/pod.c
--- xenomai-2.5.5.2/ksrc/nucleus/pod.c	2010-10-03 14:35:17.000000000 +0200
+++ xenomai-2.5.5.2.new/ksrc/nucleus/pod.c	2010-11-04 16:01:37.000000000 +0100
@@ -279,15 +279,14 @@
 	xnsched_t *sched;
 
 	trace_mark(xn_nucleus, sched_remote, MARK_NOARGS);
-#if defined(CONFIG_SMP) && defined(CONFIG_XENO_OPT_PRIOCPL)
 	sched = xnpod_current_sched();
+#if defined(CONFIG_SMP) && defined(CONFIG_XENO_OPT_PRIOCPL)
 	if (testbits(sched->status, XNRPICK)) {
 		clrbits(sched->status, XNRPICK);
 		xnshadow_rpi_check();
 	}
-#else
-	(void)sched;
 #endif /* CONFIG_SMP && CONFIG_XENO_OPT_PRIOCPL */
+	xnsched_set_resched(sched);
 	xnpod_schedule();
 }