The type used to store rtimer ticks on this platform is 32-bit integer, but the macro uses 16-bit comparison.
As a result, the output of the RTIMER_CLOCK_LT(a,b) macro was incorrect when used for comparisons between time values with sufficiently large difference.
The code to repeat this problem on mbxxx platform:
rtimer_clock_t a = 6 * RTIMER_ARCH_SECOND;
rtimer_clock_t b = 0;
printf("%d\n", RTIMER_CLOCK_LT(a,b)); // expected output: "0", actual: "1"
7dcfe77fba