model: bugfix - rearrange debug message
authorBrian Norris <banorris@uci.edu>
Thu, 3 May 2012 21:01:58 +0000 (14:01 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 3 May 2012 21:10:44 +0000 (14:10 -0700)
This debug message depends on 'exploring' still being a valid reference.
However, we immediately explore one step via get_next_replay_thread(), which
could discard this Backtrack object. So print the debug message before doing
any exploration of the next execution stage.

model.cc

index 7a29e00b6e2be472dd519e7674fa43769f998499..aba3e8bc0c1783f87cad0c9b5b60b5ba9e3ae4c3 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -142,14 +142,15 @@ bool ModelChecker::next_execution()
        print_summary();
        if ((exploring = model->get_next_backtrack()) == NULL)
                return false;
-       model->reset_to_initial_state();
-       nextThread = get_next_replay_thread();
 
        if (DBG_ENABLED()) {
                printf("Next execution will diverge at:\n");
                exploring->get_diverge()->print();
                print_list(exploring->get_trace());
        }
+
+       model->reset_to_initial_state();
+       nextThread = get_next_replay_thread();
        return true;
 }