X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=136898e913808803972f63d5b7bcd67b1b945a5e;hb=8127a0c80483af6e238f8cf2b6910a1e7da22416;hp=70ea4cd6534a9910ac176c1f497882e1ae6d3395;hpb=b1973d1489912939fb31e02a1c739bfa42cbc98c;p=c11tester.git

diff --git a/model.cc b/model.cc
index 70ea4cd6..136898e9 100644
--- a/model.cc
+++ b/model.cc
@@ -488,8 +488,10 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
 	Thread* next = getNextThread();
 	if (next != nullptr) 
 		handleNewValidThread(old, next);
-	else
+	else {
+		old->set_state(THREAD_READY);	// Just to avoid the first ASSERT in ModelExecution::take_step 
 		handleChosenThread(old);
+	}
 
 	return old->get_return_value();
 }
@@ -593,8 +595,8 @@ void ModelChecker::run()
 	initstate(423121, random_state, sizeof(random_state));
 	checkfree = params.checkthreshold;
 	for(int exec = 0;exec < params.maxexecutions;exec++) {
+		chosen_thread = init_thread;
 		do {
-			chosen_thread = init_thread;
 			thread_chosen = false;
 			curr_thread_num = 1;
 			startRunExecution(&system_context);