diff --git a/CHANGES.md b/CHANGES.md
index e854cf4..fdd8590 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -4,6 +4,13 @@ All notable changes to this project will be documented in this file.
 
 ## [Unreleased]
 * Added CHANGES.md to track changes between releases.
+* Added the collection of platform-independent performance statistics.
+* Added `bdd_used_nodes_count()` that counts the number of used nodes.
+* Replaced static `CACHESTATS` by non-static `cachestats.enabled`, which is adaptable by user and configurable per BDD factory instance.
+* Removed global JVM shutdown hook, that prints cache statistics to `stdout`, from `JFactory`.
+* Cache statistics are now measured using `longs` rather than `ints` to reduce integer overflow issues.
+* Added `opAccess` statistic to cache statistics.
+* Added functionality to reset statistics.
 
 ## [1.0.1] - 2020-03-17
 * Updated SCM URL for proper Maven Central metadata.
diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java
index 850246d..614df62 100644
--- a/src/main/java/com/github/javabdd/BDDFactory.java
+++ b/src/main/java/com/github/javabdd/BDDFactory.java
@@ -3,6 +3,7 @@
 // Licensed under the terms of the GNU LGPL; see COPYING for details.
 package com.github.javabdd;
 
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.BitSet;
 import java.util.Collection;
@@ -1235,16 +1236,20 @@ public ReorderStats getReorderStats() {
      * Stores statistics about the operator cache.
      * 
      * @author jwhaley
+     * @author sthuijsman
+     * @author mgoorden
      * @version $Id: BDDFactory.java 480 2010-11-16 01:29:49Z robimalik $
      */
     public static class CacheStats {
-        public int uniqueAccess;
-        public int uniqueChain;
-        public int uniqueHit;
-        public int uniqueMiss;
-        public int opHit;
-        public int opMiss;
-        public int swapCount;
+        protected boolean enabled = false;
+        public long uniqueAccess;
+        public long uniqueChain;
+        public long uniqueHit;
+        public long uniqueMiss;
+        public long opAccess;
+        public long opHit;
+        public long opMiss;
+        public long swapCount;
         
         protected CacheStats() { }
         
@@ -1253,11 +1258,31 @@ void copyFrom(CacheStats that) {
             this.uniqueChain = that.uniqueChain;
             this.uniqueHit = that.uniqueHit;
             this.uniqueMiss = that.uniqueMiss;
+            this.opAccess = that.opAccess;
             this.opHit = that.opHit;
             this.opMiss = that.opMiss;
             this.swapCount = that.swapCount;
         }
         
+        public void enableMeasurements() {
+        	enabled = true;
+        }
+        
+        public void disableMeasurements() {
+            enabled = false;
+        }
+        
+        public void resetMeasurements() {
+            uniqueAccess = 0;
+            uniqueChain = 0;
+            uniqueHit = 0;
+            uniqueMiss = 0;
+            opAccess = 0;
+            opHit = 0;
+            opMiss = 0;
+            swapCount = 0;
+        }
+        
         /* (non-Javadoc)
          * @see java.lang.Object#toString()
          */
@@ -1294,6 +1319,9 @@ public String toString() {
             else
                 sb.append((float)0);
             sb.append(newLine);
+            sb.append("Operator Access:  ");
+            sb.append(opAccess);
+            sb.append(newLine);
             sb.append("Operator Hits:  ");
             sb.append(opHit);
             sb.append(newLine);
@@ -1327,6 +1355,107 @@ public CacheStats getCacheStats() {
         return cachestats;
     }
     
+    /**
+     * Stores statistics about the maximum BDD nodes usage.
+     * 
+     * @author mgoorden
+     */
+    public static class MaxUsedBddNodesStats {
+        protected boolean enabled = false;
+        protected int maxUsedBddNodes;
+        
+        protected MaxUsedBddNodesStats() { }
+        
+        public void enableMeasurements() {
+        	enabled = true;
+        }
+        
+        public void disableMeasurements() {
+            enabled = false;
+        }
+        
+        public void resetMeasurements() {
+            maxUsedBddNodes = 0;
+        }
+        
+        public void newMeasurement(int newUsedBddNodes) {
+            maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes);
+        }
+        
+        public int getMaxUsedBddNodes() {
+        	return maxUsedBddNodes;
+        }
+    }
+    
+    /**
+     * Singleton object for maximum used BDD nodes statistics.
+     */
+    protected MaxUsedBddNodesStats maxusedbddnodesstats = new MaxUsedBddNodesStats();
+
+    /**
+     * <p>Return the current maximum used BDD nodes statistics for this BDD factory.</p>
+     *
+     * @return  maximum used BDD nodes statistics
+     */
+    public MaxUsedBddNodesStats getMaxUsedBddNodesStats() {
+        return maxusedbddnodesstats;
+    }
+    
+    /**
+     * Stores continuously statistics about the BDD nodes usage and BDD operations,
+     * where BDD operations is a proxy for time.
+     * 
+     * @author mgoorden
+     */
+    public static class ContinuousStats {
+        protected boolean enabled = false;
+        protected List<Integer> contUsedBddNodes = new ArrayList<Integer>();
+        protected List<Long> contOperations = new ArrayList<Long>();
+        
+        protected ContinuousStats() { }
+
+        public void enableMeasurements() {
+            enabled = true;
+        }
+        
+        public void disableMeasurements() {
+            enabled = false;
+        }
+        
+        public void resetMeasurements() {
+            contUsedBddNodes = new ArrayList<Integer>();
+            contOperations = new ArrayList<Long>();
+        }
+        
+        public List<Integer> getNodesStats() {
+            if (contUsedBddNodes.size() != contOperations.size()) {
+                throw new AssertionError("Incorrect data collection.");
+            }
+            return contUsedBddNodes;
+        }
+        
+        public List<Long> getOperationsStats() {
+            if (contUsedBddNodes.size() != contOperations.size()) {
+                throw new AssertionError("Incorrect data collection.");
+            }
+            return contOperations;
+        }
+    }
+    
+    /**
+     * Singleton object for continuous statistics.
+     */
+    protected ContinuousStats continuousstats = new ContinuousStats();
+    
+    /**
+     * <p>Return the current continuous statistics for this BDD factory.</p>
+     *
+     * @return  continuous statistics
+     */
+    public ContinuousStats getContinuousStats() {
+        return continuousstats;
+    }
+    
     // TODO: bdd_sizeprobe_hook
     // TODO: bdd_reorder_probe
     
diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java
index c6ae87a..f297462 100644
--- a/src/main/java/com/github/javabdd/JFactory.java
+++ b/src/main/java/com/github/javabdd/JFactory.java
@@ -38,9 +38,8 @@ public class JFactory extends BDDFactoryIntImpl {
     public static boolean FLUSH_CACHE_ON_GC = true;
     
     static final boolean VERIFY_ASSERTIONS = false;
-    static final boolean CACHESTATS = false;
     static final boolean SWAPCOUNT = false;
-
+    
     public static final String REVISION = "$Revision: 480 $";
     
     public String getVersion() {
@@ -55,17 +54,8 @@ private JFactory() { }
     public static BDDFactory init(int nodenum, int cachesize) {
         BDDFactory f = new JFactory();
         f.initialize(nodenum, cachesize);
-        if (CACHESTATS) addShutdownHook(f);
         return f;
     }
-
-    static void addShutdownHook(final BDDFactory f) {
-        Runtime.getRuntime().addShutdownHook(new Thread() {
-            public void run() {
-                System.out.println(f.getCacheStats().toString());
-            }
-        });
-    }
     
     boolean ZDD = false;
     
@@ -203,7 +193,6 @@ protected int makenode_impl(int lev, int lo, int hi) {
     public int setCacheSize(int v) { return bdd_setcachesize(v); }
     public boolean isZDD() { return ZDD; }
     public boolean isInitialized() { return bddrunning; }
-    public void done() { super.done(); bdd_done(); }
     public void setError(int code) { bdderrorcond = code; }
     public void clearError() { bdderrorcond = 0; }
     public int setMaxNodeNum(int size) { return bdd_setmaxnodenum(size); }
@@ -975,6 +964,9 @@ int bdd_not(int r) {
     int not_rec(int r) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         if (ISCONST(r))
             return 1 - r;
@@ -982,11 +974,11 @@ int not_rec(int r) {
         entry = BddCache_lookupI(applycache, NOTHASH(r));
 
         if (entry.a == r && entry.c == bddop_not) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         PUSHREF(not_rec(LOW(r)));
@@ -1035,6 +1027,9 @@ int ite_rec(int f, int g, int h) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (ISONE(f))
             return g;
         if (ISZERO(f))
@@ -1048,11 +1043,11 @@ int ite_rec(int f, int g, int h) {
 
         entry = BddCache_lookupI(itecache, ITEHASH(f, g, h));
         if (entry.a == f && entry.b == g && entry.c == h) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL(f) == LEVEL(g)) {
@@ -1112,6 +1107,9 @@ int ite_rec(int f, int g, int h) {
     int zite_rec(int f, int g, int h) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         if (ISONE(f))
             return g;
@@ -1130,11 +1128,11 @@ int zite_rec(int f, int g, int h) {
 
         entry = BddCache_lookupI(itecache, ITEHASH(f, g, h));
         if (entry.a == f && entry.b == g && entry.c == h) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL(f) == LEVEL(g)) {
@@ -1226,16 +1224,19 @@ int replace_rec(int r) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (ISCONST(r) || LEVEL(r) > replacelast)
             return r;
 
         entry = BddCache_lookupI(replacecache, REPLACEHASH(r));
         if (entry.a == r && entry.c == replaceid) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         PUSHREF(replace_rec(LOW(r)));
@@ -1438,6 +1439,9 @@ int bdd_apply(int l, int r, int op) {
     int apply_rec(int l, int r) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         if (VERIFY_ASSERTIONS) _assert(!ZDD);
         if (VERIFY_ASSERTIONS) _assert(applyop != bddop_and && applyop != bddop_or);
@@ -1475,11 +1479,11 @@ int apply_rec(int l, int r) {
             entry = BddCache_lookupI(applycache, APPLYHASH(l, r, applyop));
 
             if (entry.a == l && entry.b == r && entry.c == applyop) {
-                if (CACHESTATS)
+                if (cachestats.enabled)
                     cachestats.opHit++;
                 return entry.res;
             }
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opMiss++;
 
             if (LEVEL(l) == LEVEL(r)) {
@@ -1511,6 +1515,9 @@ int and_rec(int l, int r) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (l == r)
             return l;
         if (ISZERO(l) || ISZERO(r))
@@ -1523,11 +1530,11 @@ int and_rec(int l, int r) {
         entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and));
 
         if (entry.a == l && entry.b == r && entry.c == bddop_and) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL(l) == LEVEL(r)) {
@@ -1558,6 +1565,9 @@ int zand_rec(int l, int r) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (l == r)
             return l;
         if (ISZERO(l) || ISZERO(r))
@@ -1571,11 +1581,11 @@ else if (LEVEL(l) > LEVEL(r))
         entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and));
 
         if (entry.a == l && entry.b == r && entry.c == bddop_and) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         PUSHREF(zand_rec(LOW(l), LOW(r)));
@@ -1596,6 +1606,9 @@ int zrelprod_rec(int l, int r, int lev) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (l == r)
             return zquant_rec(l, lev);
         if (ISZERO(l) || ISZERO(r))
@@ -1625,11 +1638,11 @@ int zrelprod_rec(int l, int r, int lev) {
         
         entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, bddop_and));
         if (entry.a == l && entry.b == r && entry.c == appexid) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
         
         if (LEVEL_l == LEVEL_r) {
@@ -1672,6 +1685,9 @@ int or_rec(int l, int r) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (l == r)
             return l;
         if (ISONE(l) || ISONE(r))
@@ -1683,11 +1699,11 @@ int or_rec(int l, int r) {
         entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_or));
 
         if (entry.a == l && entry.b == r && entry.c == bddop_or) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL(l) == LEVEL(r)) {
@@ -1717,6 +1733,9 @@ int or_rec(int l, int r) {
     int zor_rec(int l, int r) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         if (l == r)
             return l;
@@ -1729,11 +1748,11 @@ int zor_rec(int l, int r) {
         entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_or));
 
         if (entry.a == l && entry.b == r && entry.c == bddop_or) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL(l) == LEVEL(r)) {
@@ -1763,6 +1782,9 @@ int zor_rec(int l, int r) {
     int zdiff_rec(int l, int r) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         if (ISZERO(l) /*|| ISONE(r)*/ || l == r)
             return 0;
@@ -1774,11 +1796,11 @@ int zdiff_rec(int l, int r) {
         entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_diff));
 
         if (entry.a == l && entry.b == r && entry.c == bddop_diff) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL(l) == LEVEL(r)) {
@@ -1803,6 +1825,9 @@ int zdiff_rec(int l, int r) {
     int relprod_rec(int l, int r) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         if (VERIFY_ASSERTIONS) _assert(!ZDD);
         
@@ -1824,11 +1849,11 @@ int relprod_rec(int l, int r) {
         } else {
             entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, bddop_and));
             if (entry.a == l && entry.b == r && entry.c == appexid) {
-                if (CACHESTATS)
+                if (cachestats.enabled)
                     cachestats.opHit++;
                 return entry.res;
             }
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opMiss++;
 
             if (LEVEL_l == LEVEL_r) {
@@ -1981,6 +2006,9 @@ int varset2svartable(int r) {
     int appquant_rec(int l, int r) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         if (VERIFY_ASSERTIONS) _assert(appexop != bddop_and);
         
@@ -2027,11 +2055,11 @@ else if (LEVEL(l) > quantlast && LEVEL(r) > quantlast) {
         } else {
             entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, appexop));
             if (entry.a == l && entry.b == r && entry.c == appexid) {
-                if (CACHESTATS)
+                if (cachestats.enabled)
                     cachestats.opHit++;
                 return entry.res;
             }
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opMiss++;
 
             int lev;
@@ -2073,6 +2101,9 @@ else if (LEVEL(l) > quantlast && LEVEL(r) > quantlast) {
     int appuni_rec(int l, int r, int var) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         int LEVEL_l, LEVEL_r, LEVEL_var;
         LEVEL_l = LEVEL(l);
@@ -2098,11 +2129,11 @@ else if (ISCONST(var)) {
         } else {
             entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, appexop));
             if (entry.a == l && entry.b == r && entry.c == appexid) {
-                if (CACHESTATS)
+                if (cachestats.enabled)
                     cachestats.opHit++;
                 return entry.res;
             }
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opMiss++;
 
             int lev;
@@ -2161,6 +2192,9 @@ int unique_rec(int r, int q) {
         BddCacheDataI entry;
         int res;
         int LEVEL_r, LEVEL_q;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         LEVEL_r = LEVEL(r);
         LEVEL_q = LEVEL(q);
@@ -2174,11 +2208,11 @@ int unique_rec(int r, int q) {
         
         entry = BddCache_lookupI(quantcache, QUANTHASH(r));
         if (entry.a == r && entry.c == quantid) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL_r == LEVEL_q) {
@@ -2204,16 +2238,19 @@ int quant_rec(int r) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (r < 2 || LEVEL(r) > quantlast)
             return r;
 
         entry = BddCache_lookupI(quantcache, QUANTHASH(r));
         if (entry.a == r && entry.c == quantid) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         PUSHREF(quant_rec(LOW(r)));
@@ -2242,6 +2279,10 @@ int quant_rec(int r) {
     int zquant_rec(int r, int lev) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
 
         for (;;) {
             if (lev > quantlast)
@@ -2267,11 +2308,11 @@ int zquant_rec(int r, int lev) {
         
         entry = BddCache_lookupI(quantcache, QUANTHASH(r));
         if (entry.a == r && entry.c == quantid) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         int nlev = LEVEL(r) + 1;
@@ -2337,6 +2378,9 @@ int constrain_rec(int f, int c) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (ISONE(c))
             return f;
         if (ISCONST(f))
@@ -2348,11 +2392,11 @@ int constrain_rec(int f, int c) {
 
         entry = BddCache_lookupI(misccache, CONSTRAINHASH(f, c));
         if (entry.a == f && entry.b == c && entry.c == miscid) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL(f) == LEVEL(c)) {
@@ -2434,16 +2478,19 @@ int compose_rec(int f, int g) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (LEVEL(f) > composelevel)
             return f;
 
         entry = BddCache_lookupI(replacecache, COMPOSEHASH(f, g));
         if (entry.a == f && entry.b == g && entry.c == replaceid) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL(f) < composelevel) {
@@ -2513,16 +2560,19 @@ int veccompose_rec(int f) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+
         if (LEVEL(f) > replacelast)
             return f;
 
         entry = BddCache_lookupI(replacecache, VECCOMPOSEHASH(f));
         if (entry.a == f && entry.c == replaceid) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         PUSHREF(veccompose_rec(LOW(f)));
@@ -2694,17 +2744,20 @@ int bdd_restrict(int r, int var) {
     int restrict_rec(int r) {
         BddCacheDataI entry;
         int res;
+        
+        if (cachestats.enabled)
+            cachestats.opAccess++;
 
         if (ISCONST(r) || LEVEL(r) > quantlast)
             return r;
 
         entry = BddCache_lookupI(misccache, RESTRHASH(r, miscid));
         if (entry.a == r && entry.c == miscid) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (INSVARSET(LEVEL(r))) {
@@ -2763,6 +2816,9 @@ int simplify_rec(int f, int d) {
         BddCacheDataI entry;
         int res;
 
+        if (cachestats.enabled)
+            cachestats.opAccess++;
+        
         if (ISONE(d) || ISCONST(f))
             return f;
         if (d == f)
@@ -2773,11 +2829,11 @@ int simplify_rec(int f, int d) {
         entry = BddCache_lookupI(applycache, APPLYHASH(f, d, bddop_simplify));
 
         if (entry.a == f && entry.b == d && entry.c == bddop_simplify) {
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.opHit++;
             return entry.res;
         }
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.opMiss++;
 
         if (LEVEL(f) == LEVEL(d)) {
@@ -3432,7 +3488,33 @@ int bdd_addref(int root) {
         return root;
     }
 
+    int bdd_used_nodes_count() {
+        // Mark all used bdd nodes. 
+        // bdd_mark(n) also marks the children of n.
+        for (int r = 0; r < bddrefstacktop; r++)
+            bdd_mark(bddrefstack[r]);
+
+        for (int n = 0; n < bddnodesize; n++) {
+            if (HASREF(n)) bdd_mark(n);
+        }
+
+        // Now go through all nodes and count the number of marked ones.
+        // Initial value is 2, as we always have the zero and one terminal nodes.
+        int bddCount = 2;
+        
+        for (int n = bddnodesize - 1; n >= 2; n--) {
+            if (MARKED(n) && LOW(n) != INVALID_BDD) {
+                UNMARK(n);
+                bddCount++;
+            }
+        }
+
+        return bddCount;
+    }
+ 
     int bdd_delref(int root) {
+        bdd_add_perf_stats();
+        
         if (root == INVALID_BDD)
             bdd_error(BDD_BREAK); /* distinctive */
         if (root < 2 || !bddrunning)
@@ -3496,7 +3578,7 @@ void bdd_unmark(int i) {
     int bdd_makenode(int level, int low, int high) {
         if (VERIFY_ASSERTIONS) _assert(!ZDD);
         
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.uniqueAccess++;
 
         // check whether children are equal
@@ -3509,7 +3591,7 @@ int bdd_makenode(int level, int low, int high) {
     int zdd_makenode(int level, int low, int high) {
         if (VERIFY_ASSERTIONS) _assert(ZDD);
         
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.uniqueAccess++;
         
         // check whether high child is zero
@@ -3530,18 +3612,18 @@ private int makenode(int level, int low, int high) {
 
         while (res != 0) {
             if (LEVEL(res) == level && LOW(res) == low && HIGH(res) == high) {
-                if (CACHESTATS)
+                if (cachestats.enabled)
                     cachestats.uniqueHit++;
                 return res;
             }
 
             res = NEXT(res);
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.uniqueChain++;
         }
 
         /* No existing node => build one */
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.uniqueMiss++;
 
         /* Any free nodes to use ? */
@@ -3694,7 +3776,7 @@ void bdd_init(int initnodesize, int cs) {
 
         bdderrorcond = 0;
 
-        if (CACHESTATS) {
+        if (cachestats.enabled) {
             //cachestats = new CacheStats();
         }
 
@@ -4959,6 +5041,32 @@ int bdd_reorder_gain() {
         return (100 * (usednum_before - usednum_after)) / usednum_before;
     }
 
+    public void done() { 
+        bdd_add_perf_stats();
+        
+        super.done(); 
+        bdd_done(); 
+    }
+    
+    void bdd_add_perf_stats() {
+        // The number of currently used BDD nodes, between 0 and bddnodesize.
+        // -1 indicates that it has not yet been calculated.
+        int usedBddNodes = -1;
+        
+        if (maxusedbddnodesstats.enabled) {
+            if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count();
+            maxusedbddnodesstats.newMeasurement(usedBddNodes);
+        }
+        
+        if (continuousstats.enabled) {
+            if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count();
+            continuousstats.contUsedBddNodes.add(usedBddNodes);
+            // cachestats.opMiss is the number of BDD operations performed until now that could not
+            // be taken from the cache. Thus it approximates time. 
+            continuousstats.contOperations.add(cachestats.opMiss);
+        }
+    }
+    
     void bdd_done() {
         /*sanitycheck(); FIXME */
         //bdd_fdd_done();
@@ -5661,7 +5769,7 @@ int reorder_makenode(int var, int low, int high) {
         int hash;
         int res;
 
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.uniqueAccess++;
 
         /* Note: We know that low,high has a refcou greater than zero, so
@@ -5687,19 +5795,19 @@ int reorder_makenode(int var, int low, int high) {
 
         while (res != 0) {
             if (LOW(res) == low && HIGH(res) == high) {
-                if (CACHESTATS)
+                if (cachestats.enabled)
                     cachestats.uniqueHit++;
                 INCREF(res);
                 return res;
             }
             res = NEXT(res);
 
-            if (CACHESTATS)
+            if (cachestats.enabled)
                 cachestats.uniqueChain++;
         }
 
         /* No existing node -> build one */
-        if (CACHESTATS)
+        if (cachestats.enabled)
             cachestats.uniqueMiss++;
 
         /* Any free nodes to use ? */