[mc] Use _exit() in fork()-ed process

diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 1d19bc5..0c3a6f4 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -58,7 +58,7 @@ pid_t do_fork(F f)
   // Child-process:
   try {
     f();
   // Child-process:
   try {
     f();

-    std::exit(EXIT_SUCCESS);
+    _exit(EXIT_SUCCESS);

   }
   catch(...) {
     // The callback should catch exceptions:
   }
   catch(...) {
     // The callback should catch exceptions:


@@ -125,7 +125,7 @@ std::pair<pid_t, int> create_model_checked(char** argv)
     close(sockets[1]);
     int res = exec_model_checked(sockets[0], argv);
     XBT_DEBUG("Error in the child process creation");
     close(sockets[1]);
     int res = exec_model_checked(sockets[0], argv);
     XBT_DEBUG("Error in the child process creation");

-    exit(res);
+    _exit(res);

   });
 
   // Parent (model-checker):
   });
 
   // Parent (model-checker):