bug fix

diff --git a/model.cc b/model.cc
index 33d8e15570f4ed62f54c0f739e5f8640ecd63e46..c2de31304f577187d538075de45504a94f7019b9 100644 (file)
--- 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 93160310466d6539d0863118c048e69ebbf7621d..942d183fd2b23a025e702ea48bdf2cc29391b1f4 100644 (file)
--- 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;