diff --git a/cmake-build-debug/src/mc-sog b/cmake-build-debug/src/mc-sog
index fedc1786e6596b341ec1ffe2cafdd126a71cd5de..7214c986ebb8465572d826baaf1924619a693714 100755
Binary files a/cmake-build-debug/src/mc-sog and b/cmake-build-debug/src/mc-sog differ
diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp
index 38ebf784dcf89a61fc794994468bb7a7fab28625..cd4f52f2b3f87583972063642a1aadd6cdbd5302 100644
--- a/src/HybridSOG.cpp
+++ b/src/HybridSOG.cpp
@@ -5,6 +5,7 @@ using namespace std;
 #include <stdio.h>
 
 #include "sylvan_seq.h"
+#include "sylvan_sog.h"
 #include <sylvan_int.h>
 
 using namespace sylvan;
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 073954d55ae7ab63957647940093e3b60ad8545a..aba446daa96cb36d57a5ea561bb5bd09f431102d 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -3,7 +3,7 @@
 
 
 #include <cstdio>
-
+#include "sylvan_sog.h"
 #include "sylvan_seq.h"
 #include <sylvan_int.h>
 
@@ -24,6 +24,7 @@
 #define TAG_ACK_STATE 10
 #define TAG_ACK_SUCC 11
 #define TAG_NOTCOMPLETED 20
+#define DEBUG_GC 1
 using namespace sylvan;
 using namespace std;
 MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
@@ -33,13 +34,16 @@ MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
     lace_init ( 1, 0 );
     lace_startup ( 0, NULL, NULL );
 
+    //sylvan_set_limits ( 16LL<<30, 8, 0 );
     sylvan_set_limits ( 16LL<<30, 8, 0 );
+
     //sylvan_set_limits ( 2LL<<31, 2, 1 ); // sylvan_set_limits(2LL<<31, 2, 1);
     //sylvan_set_sizes(1LL<<27, 1LL<<31, 1LL<<20, 1LL<<22);
 
     sylvan_init_package();
     sylvan_init_ldd();
     sylvan_gc_enable();
+    displayMDDTableInfo();
     m_net=&R;
 
     m_init=init;
diff --git a/src/ModelCheckerThV2.cpp b/src/ModelCheckerThV2.cpp
index 0638d9507227c085918a422aa8381ad5dc281f5f..4729ae8373b055f29e625166df372962e4a2ef95 100644
--- a/src/ModelCheckerThV2.cpp
+++ b/src/ModelCheckerThV2.cpp
@@ -135,6 +135,7 @@ void ModelCheckerThV2::Compute_successors()
         lk.unlock();
                             
             if ( m_common_stack.try_pop ( e ) && !m_finish ) {
+
                 while ( !e.second.empty() && !m_finish ) {
                     int t = *e.second.begin();
                     e.second.erase ( t );
diff --git a/src/sylvan_sog.c b/src/sylvan_sog.c
index 833841554b9cdc5128ed6e05b6da04aa1cca3cd6..66feb488753d9642486257f0bca792d3f996fafb 100644
--- a/src/sylvan_sog.c
+++ b/src/sylvan_sog.c
@@ -117,8 +117,19 @@ MDD ldd_firing_fast ( MDD cmark, MDD minus, MDD plus ) {
         n_cmark = GETNODE ( cmark );
         }
     //cache_put3(CACHE_LDD_FIRE, cmark, minus, plus, result);
+
     return result;
     }
 
-
+void  displayMDDTableInfo()
+{
+    printf("%zu of %zu buckets filled!\n", seq_llmsset_count_marked(nodes), llmsset_get_size(nodes));
+}
+int isGCRequired()
+{
+    return (g_created>llmsset_get_size(nodes)/2);
+}
+uint32_t getCountMDD() {
+    return g_created;
+}
 
diff --git a/src/sylvan_sog.h b/src/sylvan_sog.h
index 33089a966877dbed8f62d683c246003bb82f93e9..c5e15ae245eb3e35d74f8baf5282d547998eddbc 100644
--- a/src/sylvan_sog.h
+++ b/src/sylvan_sog.h
@@ -12,6 +12,9 @@ TASK_DECL_3(MDD, lddmc_firing_lace, MDD, MDD, MDD)
 #define lddmc_firing_lace(cmark, minus, plus) CALL(lddmc_firing_lace, cmark, minus, plus)
 
 
+void  displayMDDTableInfo();
+int isGCRequired();
+uint32_t getCountMDD();
 
 #ifdef __cplusplus
 }
diff --git a/third-party/sylvan b/third-party/sylvan
index 8582330575f48f010f175d9f2da630280f4cdb10..7184c4aede8b1d95c33442862075b37f9eaae899 160000
--- a/third-party/sylvan
+++ b/third-party/sylvan
@@ -1 +1 @@
-Subproject commit 8582330575f48f010f175d9f2da630280f4cdb10
+Subproject commit 7184c4aede8b1d95c33442862075b37f9eaae899