X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=2fa54d6e9ba1e76be577ec0625f6138ee7d1c5d4;hb=35c057636dd12235368cfb9644532c7561609624;hp=7181f86977688054159da03d0c3a7921ce23c958;hpb=b5cdd7ee16b73bbfe53040d23994351f85f83785;p=model-checker.git diff --git a/model.cc b/model.cc index 7181f86..2fa54d6 100644 --- a/model.cc +++ b/model.cc @@ -383,6 +383,10 @@ void ModelChecker::set_backtracking(ModelAction *act) for(int i = low_tid; i < high_tid; i++) { thread_id_t tid = int_to_id(i); + /* Make sure this thread can be enabled here. */ + if (i >= node->get_num_threads()) + break; + /* Don't backtrack into a point where the thread is disabled or sleeping. */ if (node->get_enabled_array()[i]!=THREAD_ENABLED) continue;