model: print replay/divergence information when starting a new execution

diff --git a/model.cc b/model.cc
index 976b395db7889a123465d6ba89533503aa99a749..6fea489aa0130fc8e84d2345c9890234f922eedb 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -116,12 +116,20 @@ thread_id_t ModelChecker::advance_backtracking_state()
 
 bool ModelChecker::next_execution()
 {
+       DBG();
+
        num_executions++;
        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());
+       }
        return true;
 }