Bug fix for spsc-queue test

diff --cc model.cc
index 1e425b2ece627b877e5b33dd2d7bfde60d65b47e,078a1ce75849ebc48334958a7842b22dd6c958d1..ea8f268ff270fa8d59674570103699c1eb36eb03
--- 1/model.cc
--- 2/model.cc
+++ b/model.cc
@@@ -545,17 -544,13 +545,17 @@@ void ModelChecker::handleChosenThread(T
  
  void ModelChecker::handleChosenThread(ucontext_t *old)
  {
 -      if (execution->has_asserted())
 +      if (execution->has_asserted()) {
                finishRunExecution(old);
 +              return;
 +      }
        if (!chosen_thread)
                chosen_thread = get_next_thread();
 -      if (!chosen_thread || chosen_thread->is_model_thread())
 +      if (!chosen_thread || chosen_thread->is_model_thread()) {
                finishRunExecution(old);
- /*    if (chosen_thread->just_woken_up()) {
 +              return;
 +      }
+       if (chosen_thread->just_woken_up()) {
                chosen_thread->set_wakeup_state(false);
                chosen_thread->set_pending(NULL);
                chosen_thread = NULL;
@@@ -564,9 -559,9 +564,7 @@@
                        finishRunExecution(old);
                else
                        startRunExecution(old); 
-       } */
 -      } else
--
--      {
++      } else {
                /* Consume the next action for a Thread */
                consumeAction();