X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/48af4c8427d171d3e05d39116b02e441f2391374..78c913384603a2111abf8f170b2a2d0090aabf45:/src/mc/mc_comm_determinism.c

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index d034675fc5..37a6f9054f 100644
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -248,11 +248,6 @@ void MC_pre_modelcheck_comm_determinism(void)
   /* 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 */
@@ -398,7 +393,7 @@ void MC_modelcheck_comm_determinism(void)
       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
       } else if (visited_state != -1) {
-        XBT_DEBUG("State already visited, stop the exploration");
+        XBT_DEBUG("State already visited, exploration stopped on this path.");
       } else {
         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
                   xbt_fifo_size(mc_stack) + 1);
@@ -420,6 +415,7 @@ void MC_modelcheck_comm_determinism(void)
             XBT_INFO("Communications pattern counter-example:");
             print_communications_pattern(communications_pattern);
             MC_print_statistics(mc_stats);
+            MC_SET_STD_HEAP;
             return;
           } else if (initial_global_state->send_deterministic == 0
                      && _sg_mc_send_determinism) {
@@ -434,6 +430,7 @@ void MC_modelcheck_comm_determinism(void)
             XBT_INFO("Communications pattern counter-example:");
             print_communications_pattern(communications_pattern);
             MC_print_statistics(mc_stats);
+            MC_SET_STD_HEAP;
             return;
           }
         } else {