From eed2329ef0f23c6c80c8268b6c52f212d1aa47b4 Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Tue, 2 Apr 2013 15:40:44 +0200
Subject: [PATCH] model-checker : state at max depth may have none interleaved
 processes

---
 src/mc/mc_dpor.c | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

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{
 
-- 
2.20.1