--- a/src/core/model/time.cc	Mon Aug 19 18:30:18 2013 +0200
+++ b/src/core/model/time.cc	Wed Aug 21 15:27:21 2013 -0700
@@ -48,8 +48,8 @@
 SystemMutex &
 GetMarkingMutex ()
 {
-  static SystemMutex * g_markingMutex = new SystemMutex;
-  return *g_markingMutex;
+  static SystemMutex g_markingMutex;
+  return g_markingMutex;
 }
 
 
@@ -65,7 +65,8 @@
     {
       if (! g_markingTimes)
         {
-          g_markingTimes = new Time::MarkedTimes;
+          static MarkedTimes markingTimes;
+          g_markingTimes = & markingTimes;
         }
       else
         {
@@ -234,7 +235,7 @@
   if (g_markingTimes)
     {
       NS_LOG_LOGIC ("clearing MarkedTimes");
-      delete g_markingTimes;
+      g_markingTimes->erase (g_markingTimes->begin(), g_markingTimes->end ());
       g_markingTimes = 0;
     }
 }  // Time::ClearMarkedTimes
@@ -327,7 +328,7 @@
   // Body of ClearMarkedTimes
   // Assert above already guarantees g_markingTimes != 0
   NS_LOG_LOGIC ("clearing MarkedTimes");
-  delete g_markingTimes;
+  g_markingTimes->erase (g_markingTimes->begin(), g_markingTimes->end ());
   g_markingTimes = 0;
 
 }  // Time::ConvertTimes ()