diff --git a/src/LDDState.h b/src/LDDState.h
index 6d0c3e9c53516f87116fb5d28735eca2eac71bf1..074a25371fb442715947d9518cd7eeb44f785895 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -24,10 +24,10 @@ class LDDState {
   pair<LDDState*, int> LastEdge;
   void setLDDValue(MDD m);
   MDD getLDDValue();
-  MDD m_lddstate;
+  MDD m_lddstate=0;
   unsigned char m_SHA2[81];
   unsigned char* getSHAValue();
-  bool m_boucle;
+  bool m_boucle=false;
   bool m_blocage;
 
 
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index bcffda8ee75fb3b382fd00617826886fb3c1e765..159855c45eceb1a7955c781621adf969feba6a6b 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -245,5 +245,4 @@ ModelCheckerTh::~ModelCheckerTh() {
      {
          pthread_join(m_list_thread[i], NULL);
      }
-     cout<<"Destructor "<<endl;
 }
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
index 2790ac5845d539460dc6c95314d7a4de2a07c560..e2e73dc50c9ad663841a0764b5dc4d4d5463e54a 100644
--- a/src/SogKripkeIteratorOTF.cpp
+++ b/src/SogKripkeIteratorOTF.cpp
@@ -74,3 +74,4 @@ SogKripkeIteratorOTF::~SogKripkeIteratorOTF()
 
 static ModelCheckLace * SogKripkeIteratorOTF::m_builder;
 static spot::bdd_dict_ptr* SogKripkeIteratorOTF::m_dict_ptr;
+static LDDState SogKripkeIteratorOTF::m_deadlock;
diff --git a/src/SogKripkeIteratorOTF.h b/src/SogKripkeIteratorOTF.h
index 7a3ac826762e0446ca120669b585933198cee017..717afbf3d42aaa0800b77e7b90f5f0dd839381eb 100644
--- a/src/SogKripkeIteratorOTF.h
+++ b/src/SogKripkeIteratorOTF.h
@@ -7,7 +7,7 @@
 class SogKripkeIteratorOTF : public spot::kripke_succ_iterator
 {
 public:
-
+    static LDDState m_deadlock;
     static ModelCheckLace * m_builder;
     static spot::bdd_dict_ptr* m_dict_ptr;
   //  sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index d6ae60ab5236533cd2950b48c15820dae38c6000..f28f3244245afe7be1a8b60664279c07a660bde7 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -7,13 +7,14 @@
 SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
 {
 
-    m_lddstate->setDiv(true);
+    //m_lddstate->setDiv(true);
+    //if (m_lddstate->getLDDValue()) m_lddstate->setDeadLock(true);
     for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
         m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
     }
-   /* if (lddstate->isDeadLock()) {
-        m_lsucc.push_back(pair(,-1));
-    }*/
+   if (lddstate->isDeadLock()) {
+     m_lsucc.push_back(pair<LDDState*,int>(&m_deadlock,-1));
+    }
     if (lddstate->isDiv()) {
         m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
     }
@@ -58,8 +59,6 @@ bdd SogKripkeIteratorTh::cond()  const {
     spot::formula f=spot::formula::ap(name);
     bdd   result=bdd_ithvar((p->var_map.find(f))->second);
 
-    //cout<<"Iterator "<<__func__<<"  "<<m_current_edge<<"\n";*/
-    //cout<<"exciting "<<__func__<<endl;
     return result & spot::kripke_succ_iterator::cond();
 }
 
@@ -74,3 +73,4 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh()
 
 static ModelCheckerTh * SogKripkeIteratorTh::m_builder;
 static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
+static LDDState SogKripkeIteratorTh::m_deadlock;
diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h
index b3624d6be8d978eb81bb81169c8012e230bbafde..1a8adc86648666cca49e43359220a0faee2c8e4a 100644
--- a/src/SogKripkeIteratorTh.h
+++ b/src/SogKripkeIteratorTh.h
@@ -7,7 +7,7 @@
 class SogKripkeIteratorTh : public spot::kripke_succ_iterator
 {
 public:
-
+    static LDDState m_deadlock;
     static ModelCheckerTh * m_builder;
     static spot::bdd_dict_ptr* m_dict_ptr;
   //  sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
index 13037d583dff9c4ab330013a9537219e0ea36d74..215b455210cc9c581af731542f9ab5cae76336b9 100644
--- a/src/SogKripkeOTF.cpp
+++ b/src/SogKripkeOTF.cpp
@@ -15,6 +15,7 @@ SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder)
     SogKripkeIteratorOTF::m_builder=builder;
     SogKripkeStateOTF::m_builder=builder;
     SogKripkeIteratorOTF::m_dict_ptr=&dict_ptr;
+
     //cout<<__func__<<endl;
 }