From db17cfb8915ef5b6b2977360c05a92b1b7e01a3e Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Sat, 29 Aug 2020 01:11:59 -0700
Subject: [PATCH] bug fix

---
 model.cc   | 3 ++-
 threads.cc | 1 -
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/model.cc b/model.cc
index 33d8e155..c2de3130 100644
--- a/model.cc
+++ b/model.cc
@@ -423,7 +423,6 @@ void ModelChecker::finishRunExecution(Thread *old)
 void ModelChecker::consumeAction()
 {
 	ModelAction *curr = chosen_thread->get_pending();
-	Thread * th = thread_current();
 	chosen_thread->set_pending(NULL);
 	chosen_thread = execution->take_step(curr);
 }
@@ -463,6 +462,8 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
 	}
 	DBG();
 	Thread *old = thread_current();
+	old->set_state(THREAD_READY);
+
 	ASSERT(!old->get_pending());
 
 	if (inspect_plugin != NULL) {
diff --git a/threads.cc b/threads.cc
index 93160310..942d183f 100644
--- a/threads.cc
+++ b/threads.cc
@@ -333,7 +333,6 @@ int Thread::swap(ucontext_t *ctxt, Thread *t)
 
 int Thread::swap(Thread *t, Thread *t2)
 {
-	t->set_state(THREAD_READY);
 	t2->set_state(THREAD_RUNNING);
 	if (t == t2)
 		return 0;
-- 
2.34.1