X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=922a0d60e6daf360360c83852f70ee7e47f3cf4f;hb=44118f596eb7cd9b4b0b5037fbbf958db001accc;hp=35eefa674d43d937799acd8940e00d1b0faf4cc3;hpb=c85c272294e7208e13ee5fb8e7481ee6a3732911;p=model-checker.git

diff --git a/model.cc b/model.cc
index 35eefa6..922a0d6 100644
--- a/model.cc
+++ b/model.cc
@@ -266,10 +266,11 @@ bool ModelChecker::is_deadlocked() const
 {
 	bool blocking_threads = false;
 	for (unsigned int i = 0; i < get_num_threads(); i++) {
-		Thread *t = get_thread(int_to_id(i));
-		if (scheduler->is_enabled(t) != THREAD_DISABLED)
+		thread_id_t tid = int_to_id(i);
+		if (is_enabled(tid))
 			return false;
-		else if (!t->is_model_thread() && t->get_pending())
+		Thread *t = get_thread(tid);
+		if (!t->is_model_thread() && t->get_pending())
 			blocking_threads = true;
 	}
 	return blocking_threads;
@@ -305,7 +306,7 @@ bool ModelChecker::next_execution()
 			pending_rel_seqs->size());
 
 
-	if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+	if (isfinalfeasible() || DBG_ENABLED()) {
 		checkDataRaces();
 		print_summary();
 	}
@@ -1556,7 +1557,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 		ModelAction *last = get_last_action(int_to_id(i));
 		Thread *th = get_thread(int_to_id(i));
 		if ((last && rf->happens_before(last)) ||
-				!scheduler->is_enabled(th) ||
+				!is_enabled(th) ||
 				th->is_complete())
 			future_ordered = true;