diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index 21e6d65df06740424dd73a4853925ad98f4c67bc..a09fa9d909a69e59574458e1d3f4d789ff859af7 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -2,6 +2,7 @@
 #include <sylvan.h>
 #include <string.h>
 #include <map>
+#include "SylvanWrapper.h"
 
 LDDGraph::~LDDGraph() {
     //dtor
@@ -91,7 +92,7 @@ size_t LDDGraph::findSHAPos(unsigned char *c, bool &res) {
 void LDDGraph::insert(LDDState *c) {
     std::lock_guard<std::mutex> lock(m_mutex);
     this->m_GONodes.push_back(c);
-    m_nbStates++;
+    //m_nbStates++;
 }
 
 
@@ -133,18 +134,19 @@ void LDDGraph::printCompleteInformation() {
     long count_ldd = 0L;
     for (MetaLDDNodes::const_iterator i = m_GONodes.begin(); !(i == m_GONodes.end()); i++) {
         count_ldd += lddmc_nodecount((*i)->m_lddstate);
+        m_nbMarking+= SylvanWrapper::getMarksCount((*i)->m_lddstate);
     }
     cout << "\n\nGRAPH SIZE : \n";
     cout << "\n\tNB LDD NODES : " << count_ldd;
     cout << "\n\tNB MARKING : " << m_nbMarking;
-    cout << "\n\tNB NODES : " << m_nbStates;
+    cout << "\n\tNB NODES : " << m_GONodes.size();
     cout << "\n\tNB ARCS : " << m_nbArcs << endl;
-    cout << " \n\nCOMPLETE INFORMATION ?(y/n)\n";
+    /*cout << " \n\nCOMPLETE INFORMATION ?(y/n)\n";
     char c;
-    cin >> c;
+    cin >> c;*/
     //InitVisit(initialstate,n);
 
-    size_t n = 1;
+   /* size_t n = 1;
     //cout<<"NB BDD NODE : "<<NbBdm_current_state->getContainerProcess()dNode(initialstate,n)<<endl;
     NbBddNode(m_initialstate, n);
     // cout<<"NB BDD NODE : "<<bdd_anodecount(m_Tab,(int)m_nbStates)<<endl;
@@ -156,7 +158,7 @@ void LDDGraph::printCompleteInformation() {
     if (c == 'y' || c == 'Y') {
         size_t n = 1;
         printGraph(m_initialstate, n);
-    }
+    }*/
 }
 
 /*----------------------InitVisit()------------------------*/
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index 7d653969393c24cb0a6b29bf74cdc6922b930e4e..fbc991610080f2355d4f04e5f5cb4322209ccfec 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -32,8 +32,8 @@ class LDDGraph
 		void Reset();
 		LDDState *m_initialstate;
 		LDDState *m_currentstate;
-		long m_nbStates;
-		long m_nbMarking;
+        uint64_t m_nbStates;
+		uint64_t m_nbMarking;
 		atomic<uint32_t> m_nbArcs;
 		LDDState* find(LDDState*);
         LDDState* insertFind(LDDState*);
@@ -49,7 +49,7 @@ class LDDGraph
 		void printpredecessors(LDDState *);
 		inline void addArc()  {m_nbArcs++;}
 		void insert(LDDState*);
-		LDDGraph(CommonSOG *constuctor) {m_nbStates=m_nbArcs=m_nbMarking=0;m_constructor=constuctor;}
+		LDDGraph(CommonSOG *constuctor) {m_nbArcs=m_nbMarking=0;m_constructor=constuctor;}
 		void setInitialState(LDDState*);  //Define the initial state of this graph
 		LDDState* getInitialState() const;
 		void printCompleteInformation();
diff --git a/src/ModelCheckerThV2.cpp b/src/ModelCheckerThV2.cpp
index 3a09e768e3074b80120e721ef50513e378f38900..889895145fd2cc01f32ad009862fc5a9e7e68fcd 100644
--- a/src/ModelCheckerThV2.cpp
+++ b/src/ModelCheckerThV2.cpp
@@ -25,7 +25,7 @@ getMaxMemoryV3()
 void ModelCheckerThV2::preConfigure()
 {
 
-    lace_init ( 1, 0 );
+    lace_init ( m_nb_thread, 0 );
     lace_startup ( 0, NULL, NULL );
     size_t max = 16LL<<34;
     if ( max > getMaxMemoryV3() ) {
diff --git a/src/main.cpp b/src/main.cpp
index bc7219a0ea12cc1a3d087f47d684a45213b2bcc3..9b6e7cd38036d8d4d90e052265cdf0352a1463cb 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -245,7 +245,7 @@ int main(int argc, char **argv) {
 					DR.computeSOGLaceCanonized(g);
 					g.printCompleteInformation();
 				}
-
+                /*
 				cout << "Perform Model checking ?";
 				char c;
 				cin >> c;
@@ -292,7 +292,7 @@ int main(int argc, char **argv) {
 						file.close();
 					} else
 						std::cout << "formula is verified\n";
-				}
+				}*/
 
 			}
 		}
@@ -390,6 +390,7 @@ int main(int argc, char **argv) {
 			}
 		}
 	}
+
 	MPI_Finalize();
 	return (EXIT_SUCCESS);
 }
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index dd83c1829b3ef95cb59c700c487a1902ddcae5b4..847cf0bb681b2c79422e47291506c82a5116458e 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -32,17 +32,20 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
     if (uselace)  {
     lace_init(m_nb_thread, 10000000);
     }
-    else lace_init(1, 10000000);
+    else lace_init(1, 0);
     lace_startup(0, NULL, NULL);
 
     // Simple Sylvan initialization, also initialize MDD support
     //sylvan_set_sizes(1LL<<27, 1LL<<27, 1LL<<20, 1LL<<22);
-    sylvan_set_limits(2LL<<30, 16, 3);
+    sylvan_set_limits(16LL<<30, 8, 0);
+
+    //sylvan_set_limits(2LL<<30, 16, 3);
     //sylvan_set_sizes(1LL<<30, 2LL<<20, 1LL<<18, 1LL<<20);
     //sylvan_init_bdd(1);
     sylvan_init_package();
     sylvan_init_ldd();
     LACE_ME;
+    displayMDDTableInfo();
     /*sylvan_gc_hook_pregc(TASK(gc_start));
     sylvan_gc_hook_postgc(TASK(gc_end));
     sylvan_gc_enable();*/
@@ -65,7 +68,7 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
     m_transitionName=R.transitionName;
     m_placeName=R.m_placePosName;
 
-    cout<<"Toutes les Transitions:"<<endl;
+   /* cout<<"Toutes les Transitions:"<<endl;
     map<string,uint16_t>::iterator it2=m_transitionName.begin();
     for (;it2!=m_transitionName.end();it2++) {
         cout<<(*it2).first<<" : "<<(*it2).second<<endl;}
@@ -75,7 +78,7 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
     cout<<"Transitions observables :"<<endl;
     Set::iterator it=m_observable.begin();
     for (;it!=m_observable.end();it++) {cout<<*it<<"  ";}
-    cout<<endl;
+    cout<<endl;*/
     InterfaceTrans=R.InterfaceTrans;
     m_nbPlaces=R.places.size();
     cout<<"Nombre de places : "<<m_nbPlaces<<endl;