NUM_INSNS_RETIRED
GUEST_ASSERT(count >= NUM_INSNS_RETIRED);
GUEST_ASSERT_EQ(count, NUM_INSNS_RETIRED);
__GUEST_ASSERT(count >= NUM_INSNS_RETIRED,
NUM_INSNS_RETIRED, count);