diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index 3bde48f2d8c66b66d40318512085e16cffdc3125..b36577afce581c9fc0d5679f6d476575b8bbb2dc 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -74,3 +74,4 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh()
 static ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
 static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
 static LDDState SogKripkeIteratorTh::m_deadlock;
+static LDDState SogKripkeIteratorTh::m_div;
diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h
index 774cbd5f9826003ddfd89a7e47981195962688c5..938803db2b3cada535326c715773228d9fb4fb4f 100644
--- a/src/SogKripkeIteratorTh.h
+++ b/src/SogKripkeIteratorTh.h
@@ -8,6 +8,7 @@ class SogKripkeIteratorTh : public spot::kripke_succ_iterator
 {
 public:
     static LDDState m_deadlock;
+    static LDDState m_div;
     static ModelCheckBaseMT * 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/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index 4f2e563b1b6e609633bf212649c488a3093b7e03..ab4d48a843ef133cfcdcc8f251210272dc95ade1 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -15,7 +15,9 @@ SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder)
     SogKripkeIteratorTh::m_builder=builder;
     SogKripkeStateTh::m_builder=builder;
     SogKripkeIteratorTh::m_dict_ptr=&dict_ptr;
-    
+    SogKripkeIteratorTh::m_deadlock.setLDDValue(1);
+    SogKripkeIteratorTh::m_div.setLDDValue(0);
+    SogKripkeIteratorTh::m_div.Successors.push_back(pair<LDDState*,int>(&SogKripkeIteratorTh::m_div,-1));
 }
 
 SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {