X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=threads.cc;h=b3a1d5599fb541d340184e0e2ba0f7589c0ec5ae;hb=f472540b6ab3b65c91221f6f0790d8327333a5c2;hp=9b7954d9386b6f5390ed42a32b43a53f5f5f1ca7;hpb=68bfcf59477275db784ff4bc588d47622b750afe;p=model-checker.git

diff --git a/threads.cc b/threads.cc
index 9b7954d..b3a1d55 100644
--- a/threads.cc
+++ b/threads.cc
@@ -44,6 +44,9 @@ void thread_startup()
 
 	/* Call the actual thread function */
 	curr_thread->start_routine(curr_thread->arg);
+
+	/* Finish thread properly */
+	model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread));
 }
 
 /**