model-checker : remove useless debug message and add another one

[simgrid.git] / src / mc / mc_safety.c

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 3c4f93f..a77883f 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -45,11 +45,6 @@ void MC_pre_modelcheck_safety()
   /* Wait for requests (schedules processes) */
   MC_wait_for_requests();
 
-  if (_sg_mc_visited > 0) {
-    MC_ignore_heap(simix_global->process_to_run->data, 0);
-    MC_ignore_heap(simix_global->process_that_ran->data, 0);
-  }
-
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
@@ -217,6 +212,8 @@ void MC_modelcheck_safety(void)
           XBT_DEBUG("User max depth reached !");
         else if (visited_state == -1)
           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+        else
+          XBT_DEBUG("State already visited, exploration stopped on this path.");
 
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           /* Interleave enabled processes in the state in which they have been enabled for the first time */