From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Tue, 2 Apr 2013 13:40:44 +0000 (+0200)
Subject: model-checker : state at max depth may have none interleaved processes
X-Git-Tag: v3_9_90~412^2~61
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/eed2329ef0f23c6c80c8268b6c52f212d1aa47b4?hp=9d8ce6c58ec7d0a682ef47fde0c8199026948bb8

model-checker : state at max depth may have none interleaved processes
---

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 38ec8a76dd..7c5b9980ca 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -378,7 +378,18 @@ void MC_dpor(void)
           }
         }
 
-        max_depth_reached = 1;
+        if(MC_state_interleave_size(state) > 0){
+          max_depth_reached = 1;
+        }else{
+          /* Trash the current state, no longer needed */
+          MC_SET_RAW_MEM;
+          xbt_fifo_shift(mc_stack_safety);
+          MC_state_delete(state);
+          MC_UNSET_RAW_MEM;
+
+          max_depth_reached = 0;
+        }
+        
 
       }else{