From 33a0676006be6e35e0fa9e6bd907ca7bae5e53e2 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 6 Sep 2012 14:07:44 -0700
Subject: [PATCH] model: complete the Thread teardown during THREAD_FINISH

---
 model.cc | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/model.cc b/model.cc
index 0bb9617..56723c7 100644
--- a/model.cc
+++ b/model.cc
@@ -311,6 +311,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			Thread *wake = th->pop_wait_list();
 			scheduler->wake(wake);
 		}
+		th->complete();
 	}
 
 	/* Deal with new thread */
@@ -978,11 +979,8 @@ bool ModelChecker::take_step() {
 			ASSERT(current_action);
 			nextThread = check_current_action(current_action);
 			current_action = NULL;
-			if (!curr->is_blocked())
+			if (!curr->is_blocked() && !curr->is_complete())
 				scheduler->add_thread(curr);
-		} else if (curr->get_state() == THREAD_RUNNING) {
-			/* Stopped while running; i.e., completed */
-			curr->complete();
 		} else {
 			ASSERT(false);
 		}
-- 
2.34.1