model-checker : really (?) fix SIMCALL_MUTEX_LOCK and UNLOCK with MC

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index ca66d7b..790d1e9 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -332,6 +332,7 @@ void MC_do_the_modelcheck_for_real()
 
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     XBT_INFO("Check communication determinism");
+    mc_reduce_kind = e_mc_reduce_none;
     MC_modelcheck_comm_determinism_init();
   } else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
     if(_sg_mc_termination){
@@ -339,7 +340,6 @@ void MC_do_the_modelcheck_for_real()
       mc_reduce_kind = e_mc_reduce_none;
     }else{
       XBT_INFO("Check a safety property");
-      mc_reduce_kind = e_mc_reduce_dpor;
     }
     MC_modelcheck_safety_init();
   } else {
@@ -395,6 +395,7 @@ void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int valu
         current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t);
       complete_comm_pattern(pattern, current_comm, req->issuer->pid, backtracking);
     }
+    break;
   default:
     xbt_die("Unexpected call type %i", (int)call_type);
   }