if (isfeasibleprefix()) {
if (is_yieldblocked())
model_print(" YIELD BLOCKED");
if (scheduler->all_threads_sleeping())
model_print(" SLEEP-SET REDUNDANT");
if (isfeasibleprefix()) {
if (is_yieldblocked())
model_print(" YIELD BLOCKED");
if (scheduler->all_threads_sleeping())
model_print(" SLEEP-SET REDUNDANT");