[mc] Bug: MC was reading from the wrong region

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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 2c5ded0..4717fcd 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -216,9 +216,6 @@ void MC_pre_modelcheck_liveness(void)
 
   MC_wait_for_requests();
 
-  MC_ignore_heap(simix_global->process_to_run->data, 0);
-  MC_ignore_heap(simix_global->process_that_ran->data, 0);
-
   MC_SET_MC_HEAP;
 
   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
@@ -243,7 +240,7 @@ void MC_pre_modelcheck_liveness(void)
       initial_pair->graph_state = MC_state_new();
       initial_pair->atomic_propositions = get_atomic_propositions_values();
 
-      /* Get enabled process and insert it in the interleave set of the graph_state */
+      /* Get enabled processes and insert them in the interleave set of the graph_state */
       xbt_swag_foreach(process, simix_global->process_list) {
         if (MC_process_is_enabled(process)) {
           MC_state_interleave_process(initial_pair->graph_state, process);
@@ -426,7 +423,7 @@ void MC_modelcheck_liveness()
               next_pair->automaton_state = transition_succ->dst;
               next_pair->atomic_propositions = get_atomic_propositions_values();
 
-              /* Get enabled process and insert it in the interleave set of the next graph_state */
+              /* Get enabled processes and insert them in the interleave set of the next graph_state */
               xbt_swag_foreach(process, simix_global->process_list) {
                 if (MC_process_is_enabled(process)) {
                   MC_state_interleave_process(next_pair->graph_state, process);