diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index cca2d5e04..66113204c 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1532,7 +1532,6 @@ namespace dd {
     }
 
     void pdd_manager::gc() {
-        m_gc_generation++;
         init_dmark();
         m_free_nodes.reset();
         SASSERT(well_formed());
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index aef0eb6f7..f5ed9e790 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -208,7 +208,6 @@ namespace dd {
         rational                   m_mod2N;
         unsigned                   m_power_of_2 = 0;
         rational                   m_max_value;
-        unsigned                   m_gc_generation = 0;  ///< will be incremented on each GC
 
         void reset_op_cache();
         void init_nodes(unsigned_vector const& l2v);