diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 81a6101191ef5568e031487c27e8a77d851876b9..f805b330a661b845b774fb6f659a2d7470af44c7 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -66,7 +66,7 @@ void CNDFS::threadRun() {
  * Build initial state of the product automata
  */
 void CNDFS::getInitialState() {
-    mInitStatePtr = new myState_t;
+    mInitStatePtr = new myState_t(mNbTh);
     mInitStatePtr->left = mMcl->getInitialMetaState();
     mInitStatePtr->right = mAa->get_init_state();
     mInitStatePtr->isAcceptance = mAa->state_is_accepting(mAa->get_init_state());
@@ -77,7 +77,7 @@ void CNDFS::getInitialState() {
 
 //this function is to build a state with list of successor initially null
 myState_t *CNDFS::buildState(LDDState *left, spot::state *right, bool acc, bool constructed, bool cyan) {
-    myState_t *buildStatePtr = new myState_t;
+    myState_t *buildStatePtr = new myState_t(mNbTh);
     buildStatePtr->left = left;
     buildStatePtr->right = (spot::twa_graph_state *) right;
     buildStatePtr->isAcceptance = acc;
@@ -101,8 +101,6 @@ std::ostream &operator<<(std::ostream &Str, myState_t *state) {
 void CNDFS::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread) {
 //    if(finish) return;
     Rp.push_back(state);
-    std::mt19937 g(rd());
-    std::shuffle(state->new_successors.begin(), state->new_successors.end(), g);
     for (const auto &succ: state->new_successors) {
 //        cout << "dfs red 1 "  << succ.first->cyan[idThread]<< endl;
         if (succ.first->cyan[idThread]) {
@@ -112,7 +110,7 @@ void CNDFS::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread)
             exit(0);
         }
         // unvisited and not red state
-        if ((find(Rp.begin(), Rp.end(), state) != Rp.end()) && !succ.first->red){
+        if ((find(Rp.begin(), Rp.end(), succ.first) != Rp.end()) && !succ.first->red){
             dfsRed(succ.first, Rp, idThread);
         }
 
@@ -131,7 +129,7 @@ myState_t *CNDFS::isStateBuilt(LDDState *sogState, spot::twa_graph_state *spotSt
 }
 
 //compute new successors of a product state
-void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
+void CNDFS::computeSuccessors(myState_t *state, const vector<spot::formula>& ap_sog) {
 
     if (state->succState == SuccState::done) return;
     std::unique_lock lk(mMutexStatus);
@@ -196,13 +194,12 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
 
 
 //Perform the dfsBlue
-void CNDFS::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread, vector<spot::formula> ap_sog) {
+void CNDFS::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread, const vector<spot::formula>& ap_sog) {
 //    if(finish) std::terminate();  stop current thread
 //    if(finish) return;
     state->cyan[idThread] = true;
     computeSuccessors(state, ap_sog);
-    std::mt19937 g(rd());
-    std::shuffle(state->new_successors.begin(), state->new_successors.end(), g);
+
     for (const auto &succ: state->new_successors) {
 //        cout << "cyan " << succ.first->cyan[idThread] << endl;
         if (!succ.first->blue && !succ.first->cyan[idThread]) {
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 1c51773592794f193ef48a0ef832f8356d534d8c..3a4d27f968967ee051d22d1f33921f082bdf45c4 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -22,12 +22,19 @@ static constexpr uint8_t MAX_THREADS = 64;
 
 enum class SuccState {notyet,doing,done};
 struct myState_t {
+    myState_t(uint16_t n) {
+        cyan=new bool[n];
+        for (uint16_t i=0;i<n;i++) cyan[i]=false;
+    }
+    ~myState_t() {
+        delete [] cyan;
+    }
     LDDState *left;
     const spot::twa_graph_state *right;
     vector<pair<struct myState_t *, int>> new_successors;
     bool isAcceptance {false};
     bool isConstructed {false};
-    array<bool, MAX_THREADS> cyan {false};
+    bool* cyan ;
     atomic<bool> blue{false};
     atomic<bool> red{false};
     SuccState succState {SuccState::notyet};
@@ -60,7 +67,7 @@ private:
 
     void threadRun();
 
-    void computeSuccessors(myState_t *state, vector<spot::formula> ap_sog);
+    void computeSuccessors(myState_t *state, const vector<spot::formula>& ap_sog);
 
     myState_t *buildState(LDDState *left, spot::state *right, bool acc, bool constructed, bool cyan);
 
@@ -72,7 +79,7 @@ public:
 
     virtual ~CNDFS();
 
-    void dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread,vector<spot::formula> ap_sog);
+    void dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread,const vector<spot::formula>& ap_sog);
 
     void dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread);
 
diff --git a/src/algorithm/CndfsV2.cpp b/src/algorithm/CndfsV2.cpp
index 60bdf27b19afd44a1a7c562969d3bb791e17b7d6..b8417b4b32c5ae735640709a12455948a347c1ba 100644
--- a/src/algorithm/CndfsV2.cpp
+++ b/src/algorithm/CndfsV2.cpp
@@ -64,7 +64,7 @@ void CndfsV2::threadRun() {
  * Build initial state of the product automata
  */
 void CndfsV2::getInitialState() {
-    mInitStatePtr = new myState_t;
+    mInitStatePtr = new myState_t(mNbTh);
     mInitStatePtr->left = mMcl->getInitialMetaState();
     mInitStatePtr->right = mAa->get_init_state();
     mInitStatePtr->isAcceptance = mAa->state_is_accepting(mAa->get_init_state());
@@ -94,7 +94,7 @@ const spot::twa_graph_state* CndfsV2::getSuccessorFromBA(  const spot::twa_graph
 
 //this function is to build a state with list of successor initially null
 myState_t *CndfsV2::buildState(myState_t *state, pair<spot::formula, int > tr) {
-    myState_t *buildStatePtr = new myState_t;
+    myState_t *buildStatePtr = new myState_t(mNbTh);
     buildStatePtr->left = getSuccessorFromSOG(state->left,tr);
     buildStatePtr->right = getSuccessorFromBA(state->right,tr);
     buildStatePtr->isAcceptance =  mAa->state_is_accepting(buildStatePtr->right);