bug fix

[c11tester.git] / model.cc

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) {