diff --git a/prism/include/DebugJDD.h b/prism/include/DebugJDD.h
index b7963c20..bc9f4b0e 100644
--- a/prism/include/DebugJDD.h
+++ b/prism/include/DebugJDD.h
@@ -7,8 +7,6 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
-#undef jdd_DebugJDD_debugEnabled
-#define jdd_DebugJDD_debugEnabled 0L
 /*
  * Class:     jdd_DebugJDD
  * Method:    DebugJDD_GetRefCount
@@ -29,3 +27,14 @@ JNIEXPORT jlongArray JNICALL Java_jdd_DebugJDD_DebugJDD_1GetExternalRefCounts
 }
 #endif
 #endif
+/* Header for class jdd_DebugJDD_DebugJDDNode */
+
+#ifndef _Included_jdd_DebugJDD_DebugJDDNode
+#define _Included_jdd_DebugJDD_DebugJDDNode
+#ifdef __cplusplus
+extern "C" {
+#endif
+#ifdef __cplusplus
+}
+#endif
+#endif
diff --git a/prism/src/jdd/DebugJDD.java b/prism/src/jdd/DebugJDD.java
index bf3da6e5..1f8c9c28 100644
--- a/prism/src/jdd/DebugJDD.java
+++ b/prism/src/jdd/DebugJDD.java
@@ -4,6 +4,7 @@
 //	Authors:
 //	* Vojtech Forejt <vojtech.forejt@cs.ox.ac.uk> (University of Oxford)
 //	* Christian von Essen <christian.vonessen@imag.fr> (VERIMAG)
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -27,11 +28,14 @@
 
 package jdd;
 
+import java.util.ArrayList;
 import java.util.HashMap;
-import java.util.Iterator;
-import java.util.LinkedList;
+import java.util.HashSet;
+import java.util.LinkedHashMap;
 import java.util.List;
-import java.util.ListIterator;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.TreeMap;
 
 public class DebugJDD
 {
@@ -48,157 +52,293 @@ public class DebugJDD
 	}
 
 	/**
-	 * determines if the debugging of JDD nodes is enabled.
+	 * A DebugJDDNode extends a JDDNode with additional information
+	 * useful for tracking refs/derefs and tracing.
 	 */
-	public static final boolean debugEnabled = false;
+	protected static class DebugJDDNode extends JDDNode {
 
-	/**
-	 * Where stack traces are kept.
-	 * Key: hashcode of a JDDNode
-	 * Value: stack trace from the moment the JDDNode was constructed.
-	 */
-	protected static HashMap<Integer, StackTraceElement[]> stackTraces;
+		/** A static counter that is used to provide a unique ID for each JDDNode */
+		private static long nextId = 0;
+
+		/**
+		 * The ID for this JDDNode. In contrast with the DdNode* ptr, this will be
+		 * stable across PRISM invocations and can thus be used for tracing.
+		 */
+		private long id;
+
+		/** The balance of reference/dereference calls this specific JDDNode */
+		private int nodeRefs = 0;
+
+		/**
+		 * Constructor, with DdNode* ptr.
+		 * @param ptr the DdNode pointer in CUDD
+		 * @param isReferenced Does this JDDNode already have a reference
+		 *                     (like for ptrToNode) or not (like for getThen / getElse)
+		 */
+		public DebugJDDNode(long ptr, boolean isReferenced)
+		{
+			// instantiate underlying JDDNode
+			super(ptr);
+			// generate and store globally unique ID
+			id = nextId++;
+			// the initial number of references for this JDDNode
+			nodeRefs = (isReferenced ? 1 : 0);
+			if (isReferenced) {
+				// increase javaRefs counter for this ptr
+				int jrefs = getJavaRefCount(ptr());
+				javaRefs.put(ptr(), jrefs+1);
+			}
+			// store to keep track of this DebugJDDNode
+			DebugJDD.addToSet(this);
+		}
+
+		/** Get the ID of this node */
+		public long getID()
+		{
+			return id;
+		}
+
+		/** Increment the reference count for this JDDNode */
+		public void incRef()
+		{
+			// increment count for node
+			nodeRefs++;
+			// increment javaRefs counter for this ptr
+			int jrefs = getJavaRefCount(ptr());
+			javaRefs.put(ptr(), jrefs + 1);
+		}
+
+		/** Decrement the reference count for this JDDNode */
+		public void decRef()
+		{
+			// decrement count for node
+			nodeRefs--;
+			// decrement javaRefs counter for this ptr
+			int jrefs = getJavaRefCount(ptr()) - 1;
+			javaRefs.put(ptr(), jrefs);
+
+			// Checks:
+			// (1) There is a negative number of Java references for the DdNode pointer
+			if (jrefs < 0) {
+				throw new RuntimeException("DebugJDD: The number of Java references is negative for ptr=0x"+Long.toHexString(ptr())+", ID="+getID()+", Java refs = "+jrefs+", CUDD refs = "+DebugJDD_GetRefCount(ptr()));
+			}
+			// (2) There are more Java references than Cudd references
+			if (jrefs > DebugJDD_GetRefCount(ptr())) {
+				throw new RuntimeException("DebugJDD: More Java refs than CUDD refs for ptr=0x"+Long.toHexString(ptr())+", ID="+getID()+", Java refs = "+jrefs+", CUDD refs = "+DebugJDD_GetRefCount(ptr()));
+			}
+			// (3) This node has more refs than there are Java refs in total
+			if (jrefs < getNodeRefs()) {
+				throw new RuntimeException("DebugJDD: JDDNode has more refs than Java refs in total?! ID="+getID()+", refs = "+getNodeRefs()+", Java refs = "+jrefs+", CUDD refs = "+DebugJDD_GetRefCount(ptr()));
+			}
+		}
+
+		/** Get the number of active references for this JDDNode */
+		public int getNodeRefs()
+		{
+			return nodeRefs;
+		}
+	}
 
 	/**
-	 * Keeps track of refs and derefs made in Java
-	 * Key: hashcode of a JDDNode
-	 * Value: 1 + (number of times the node was refed) - (number of times the node was derefed)
+	 * Flag, determines if the debugging of JDD nodes is enabled.
 	 */
-	protected static HashMap<Integer, Integer> localCounters;
+	public static boolean debugEnabled = false;
 
 	/**
-	 * Keeps track of instances of JDDNode pointing to (native) DdNode
-	 * Key: pointer to a DdNode
-	 * Value: list of hashcodes of JDDNodes pointing to the DdNode
+	 * Map from DebugJDDNode IDs to DebugJDDNode.
+	 * LinkedHashMap to ensure that iterating over the map returns the
+	 * DebugJDDNodes in a consistent order, sorted by ID.
 	 */
-	protected static HashMap<Long, List<Integer>> instances;
+	protected static LinkedHashMap<Long, DebugJDDNode> nodes = new LinkedHashMap<Long, DebugJDDNode>();
+
+	/** A map from DdNode pointers to the current sum of the nodeRefs of all JDDNodes for that pointer */
+	protected static HashMap<Long, Integer> javaRefs = new HashMap<Long, Integer>();
 
-	protected static void addToSet(JDDNode node, int count)
+	/** An optional set of DebugJDDNode IDs that will be traced */
+	protected static HashSet<Long> traceIDs = null;
+
+	/** Enable debugging */
+	public static void enable()
 	{
-		//not thread safe
-		if (instances == null) {
-			instances = new HashMap<Long, List<Integer>>();
-			localCounters = new HashMap<Integer, Integer>();
-			stackTraces = new HashMap<Integer, StackTraceElement[]>();
+		debugEnabled = true;
+	}
+	/** Activate tracing for the DebugJDDNode with ID id */
+	public static void enableTracingForID(long id) {
+		if (traceIDs == null) {
+			traceIDs = new HashSet<Long>();
 		}
-
-		int hc = System.identityHashCode(node);
-		if (instances.containsKey(node.ptr())) {
-			long ptr = node.ptr();
-			instances.get(ptr).add(hc);
-		} else {
-			long ptr = node.ptr();
-			List<Integer> al = new LinkedList<Integer>();
-			al.add(hc);
-			instances.put(ptr, al);
+		traceIDs.add(id);
+		System.out.println("DebugJDD: Enable tracing for "+id);
+		enable();  // tracing implies debugging
+	}
+	/** Store a DebugJDDNode for tracking of the references */
+	protected static void addToSet(DebugJDDNode node)
+	{
+		if (nodes.put(node.getID(), node) != null) {
+			// implementation error, should not happen
+			throw new RuntimeException("DebugJDD: Adding the same JDDNode multiple times, ID="+node.getID());
 		}
-		localCounters.put(hc, count);
-
-		StackTraceElement[] st = Thread.currentThread().getStackTrace();
-		//ignore first two elements which are Thread and this constructor
-		int num = st.length - 2;
-		StackTraceElement[] creator = new StackTraceElement[num];
-		for (int i = 0; i < num; i++) {
-			creator[i] = st[i + 2];
+		if (traceIDs != null && traceIDs.contains(node.id)) {
+			trace("create", node);
 		}
-		stackTraces.put(hc, creator);
 	}
 
+	/** Notification from JDD.Deref(node) */
 	protected static void decrement(JDDNode node)
 	{
-		int hc = System.identityHashCode(node);
-		int newValue = localCounters.get(hc) - 1;
+		if (!(node instanceof DebugJDDNode)) {
+			// deref of a node that is not wrapped in a DebugJDDNode
+			//  -> probably came from JDDNode.getThen()/getElse(), should not be derefed
+			throw new RuntimeException("DebugJDD: Trying to Deref a plain JDDNode (obtained from getThen()/getElse()?)");
+		}
+		DebugJDDNode dNode = (DebugJDDNode) node;
+		if (dNode.getNodeRefs() == 0) {
+			// This is only a warning as currently there are places
+			// where referencing / derefencing happens across multiple JDDNodes
+			System.out.println("Warning, DebugJDD: Deref of a JDDNode that has 0 references, ID = "+dNode.getID());
+			printStack(0);
+		}
+		dNode.decRef();
 		int cuddRefCount = DebugJDD_GetRefCount(node.ptr());
-		assert cuddRefCount > 0;
-		assert cuddRefCount - 1 >= newValue;
-		if (newValue < 0 && cuddRefCount == newValue) {
-			System.out.println("Dereferencing node " + node + " too often. Printing stack trace where it was created.");
-			//print only top 5 methods from stack
-			int i = 0;
-			for (StackTraceElement st : stackTraces.get(hc)) {
-				if (i++ > 5) {
-					break;
-				}
-				System.out.println("  " + st.toString());
-			}
-			assert false;
+		if (cuddRefCount <= 0) {
+			throw new RuntimeException("DebugJDD: Trying to deref a JDDNode with a non-positive CUDD ref count, ptr=0x"+Long.toHexString(dNode.ptr())+", ID = "+dNode.getID()+", Java ref = "+getJavaRefCount(dNode.ptr())+", CUDD refs = "+cuddRefCount);
+		}
+		if (traceIDs != null && traceIDs.contains(dNode.id)) {
+			trace("deref", dNode);
 		}
-
-		localCounters.put(hc, newValue);
 	}
 
+	/** Notification from JDD.Ref(node) */
 	protected static void increment(JDDNode node)
 	{
-		int hc = System.identityHashCode(node);
-		int newValue = localCounters.get(hc) + 1;
-		int cuddRefCount = DebugJDD_GetRefCount(node.ptr());
-		assert cuddRefCount + 1 >= newValue; 
-		localCounters.put(hc, newValue);
+		if (!(node instanceof DebugJDDNode)) {
+			// ref of a node that is not wrapped in a DebugJDDNode
+			//  -> probably came from JDDNode.getThen()/getElse(), should not be refed
+			throw new RuntimeException("DebugJDD: Trying to Ref a plain JDDNode (obtained from getThen()/getElse()?)");
+		}
+		DebugJDDNode dNode = (DebugJDDNode) node;
+		dNode.incRef();
+		if (traceIDs != null && traceIDs.contains(dNode.id)) {
+			trace("ref", dNode);
+		}
 	}
 
 	public static void endLifeCycle()
 	{
-		// Kick everybody who hasn't got a reference count higher than zero out
-		for (Iterator<Long> itt = instances.keySet().iterator(); itt.hasNext(); ) {
-			Long ptr = itt.next();
-			for (Iterator<Integer> it = instances.get(ptr).iterator(); it.hasNext(); ) {
-				int localRefCount = localCounters.get(it.next());
-				if (localRefCount != 0) {
-					it.remove();
-				}
-			}
-			if (instances.get(ptr).isEmpty()) {
-				itt.remove();
-			}
+		// Get the external reference count from CUDD
+		Map<Long, Integer> externalRefCounts = getExternalRefCounts();
+		if (externalRefCounts.size() == 0) {
+			// everthing is fine
+			return;
 		}
-		for (Long ptr : instances.keySet()) {
-			//check if cudd has nonzero number of references
-			int cuddRefCount = DebugJDD_GetRefCount(ptr);
-			if (cuddRefCount != 0) {
-				//check if there is a JDD object with nonzero refcount
-				boolean hasSuspicious = false;
-				for (Integer hc : instances.get(ptr)) {
-					int localRefCount = localCounters.get(hc);
-					if (localRefCount > 0) {
-						hasSuspicious = true;
-						break;
+
+		System.out.println("\nWarning: Found " + externalRefCounts.size() + " leaked JDDNode references.");
+		System.out.flush();
+		for (Entry<Long, Integer> extRef : externalRefCounts.entrySet()) {
+			long ptr = extRef.getKey();
+			List<DebugJDDNode> matchingNodes = new ArrayList<DebugJDDNode>();
+			List<DebugJDDNode> posRewNodes = new ArrayList<DebugJDDNode>();
+			for (DebugJDDNode node : nodes.values()) {
+				if (node.ptr() == ptr) {
+					// node matches
+					matchingNodes.add(node);
+					// node still has positive reference count
+					if (node.getNodeRefs() > 0) {
+						posRewNodes.add(node);
 					}
 				}
+			}
 
-				//if !hasSuspicious, there is no useful output we could give.
-				//Either it's false alarm, or the problem is in c++
-				if (!hasSuspicious)
-					continue;
-				System.out.println("WARNING: there are nodes with nonzero references, printing debug info. "
-						+ "Note that the stack traces below are from moments JDDNodes were "
-						+ "created. The actual problem can be elsewhere where the node is used");
-				//print warning together with suspicious nodes
-				System.out.println("Node " + new JDDNode(ptr, false) + " has " + cuddRefCount + " reference(s), printing out stack traces of suspicious node instances:");
-				boolean first = true;
-				for (Integer hc : instances.get(ptr)) {
-					int localRefCount = localCounters.get(hc);
-					if (localRefCount != 0) {
-						if (!first) {
-							System.out.println(" &");
-							//first=false;
-						} else {
-							first = false;
-						}
-						//print only top 5 methods from stack
-						int i = 0;
-						for (StackTraceElement st : stackTraces.get(hc)) {
-							if (i++ > 8) {
-								break;
-							}
-							System.out.println("  " + st.toString());
-						}
-					}
+			System.out.println("DdNode ptr=0x" + Long.toHexString(ptr)+", "+nodeInfo(ptr)+" has "+extRef.getValue()+" remaining external references.");
+			if (posRewNodes.size() > 0) {
+				System.out.println(" Candidates:");
+				for (DebugJDDNode node : posRewNodes) {
+					System.out.println("  ID="+node.getID()+" with "+node.getNodeRefs()+" references");
+				}
+			} else {
+				System.out.println(" No candidates, here are all JDDNodes for that DdNode:");
+				for (DebugJDDNode node : matchingNodes) {
+					System.out.println("  ID="+node.getID()+" with "+node.getNodeRefs()+" references");
 				}
 			}
 		}
 	}
-	
+
+	/** Get the CUDD reference count for the pointer of the JDDNode */
 	public static int getRefCount(JDDNode n) {
 		return DebugJDD_GetRefCount(n.ptr());
 	}
+
+	/** Get the number of DebugJDDNodes that reference the pointer */
+	private static int getJavaRefCount(long ptr) {
+		Integer jrefs = javaRefs.get(ptr);
+		if (jrefs == null) return 0;
+		return jrefs;
+	}
+
+	/** Get a map, mapping DdNode pointers to the external reference counts expected by CUDD */
+	public static Map<Long, Integer> getExternalRefCounts()
+	{
+		Map<Long, Integer> result = new TreeMap<Long, Integer>();
+		// Array consists of (pointer, count) pairs
+		long[] externalRefCounts = DebugJDD_GetExternalRefCounts();
+		int i=0;
+		while (i<externalRefCounts.length) {
+			long node = externalRefCounts[i++];
+			int count = (int)externalRefCounts[i++];
+			result.put(node, count);
+
+		}
+
+		return result;
+	}
+
+	/** Get a string with more detailed info for a DdNode pointer */
+	private static String nodeInfo(long ptr)
+	{
+		if (JDDNode.DDN_IsConstant(ptr)) {
+			return "constant("+JDDNode.DDN_GetValue(ptr)+"), CUDD refs="+DebugJDD_GetRefCount(ptr);
+		} else {
+			return "var("+JDDNode.DDN_GetIndex(ptr)+"), CUDD refs="+DebugJDD_GetRefCount(ptr);
+		}
+	}
+
+	/** Log information about the action performed on the DebugJDDNode */
+	private static void trace(String action, DebugJDDNode dNode)
+	{
+		System.out.println("\ntrace("+action+",ID="+dNode.getID()+") = "+dNode.getNodeRefs()+" refs (total = "+DebugJDD_GetRefCount(dNode.ptr())+", local="+javaRefs.get(dNode.ptr())+")");
+		printStack(0);
+	}
+
+	/** Print the current stack trace, omitting initial java.lang and jdd.DebugJDD frames.
+	 * @param limit Limit on the number of frames to print, 0 = no limit
+	 */
+	private static void printStack(int limit)
+	{
+		// apparently, the following is more efficient than calling Thread.currentThread.getStackTrace()
+		StackTraceElement[] stack = (new Throwable()).getStackTrace();
+		boolean foundStart = false;
+		int printed = 0;
+		for (StackTraceElement ste : stack) {
+			String st = ste.toString();
+			if (!foundStart) {
+				if (st.startsWith("java.lang") || st.startsWith("jdd.DebugJDD")) {
+					// skip
+					continue;
+				} else {
+					foundStart = true;
+					// continue below
+				}
+			}
+			if (limit > 0 && printed++ >= limit) {
+				System.out.println("  ...");
+				break;
+			} else {
+				System.out.println("  at " + st);
+			}
+		}
+		System.out.println();
+		System.out.flush();
+	}
+
 }
diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java
index 98aacb98..e2a455bc 100644
--- a/prism/src/jdd/JDD.java
+++ b/prism/src/jdd/JDD.java
@@ -1394,6 +1394,9 @@ public class JDD
 		if (ptr == 0L) {
 			throw new CuddOutOfMemoryException();
 		}
+		if (DebugJDD.debugEnabled) {
+			return new DebugJDD.DebugJDDNode(ptr, true);
+		}
 		return new JDDNode(ptr);
 	}
 
diff --git a/prism/src/jdd/JDDNode.java b/prism/src/jdd/JDDNode.java
index 11395650..6670ef35 100644
--- a/prism/src/jdd/JDDNode.java
+++ b/prism/src/jdd/JDDNode.java
@@ -49,20 +49,14 @@ public class JDDNode
 		}
 	}
 
-	public JDDNode(long p, boolean increased_reference)
+	/**
+	 * Protected constructor from a DdNode pointer.
+	 * In general, to get a JDDNode from a pointer,
+	 * use JDD.ptrToNode().
+	 */
+	protected JDDNode(long p)
 	{
 		ptr = p;
-		if (DebugJDD.debugEnabled)
-			DebugJDD.addToSet(this, increased_reference ? 1 : 0);
-	}
-	
-	public JDDNode(long p) {
-		this(p, true);
-	}
-	
-	public JDDNode(JDDNode dd)
-	{
-		this(dd.ptr());
 	}
 	
 	public long ptr()
@@ -85,18 +79,34 @@ public class JDDNode
 		return DDN_GetValue(ptr);
 	}
 
+	/**
+	 * Returns the Then child of a (non-constant) JDDNode.
+	 * <br>
+	 * This method does NOT increase the reference count of the returned
+	 * node, it is therefore illegal to call JDD.Deref on the result.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
 	public JDDNode getThen()
 	{
 		assert !this.isConstant();
-		// TODO I believe that this breaks debug reference counting
-		// JDDNode will create a reference to this, but DDN_GetThen will not.
-		return new JDDNode(DDN_GetThen(ptr), false);
+
+		// just return the node, even if DebugJDD is enabled
+		return new JDDNode(DDN_GetThen(ptr));
 	}
-	
+
+	/**
+	 * Returns the Else child of a (non-constant) JDDNode.
+	 * <br>
+	 * This method does NOT increase the reference count of the returned
+	 * node, it is therefore illegal to call JDD.Deref on the result.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
 	public JDDNode getElse()
 	{
 		assert !this.isConstant();
-		return new JDDNode(DDN_GetElse(ptr), false);
+
+		// just return the node, even if DebugJDD is enabled
+		return new JDDNode(DDN_GetElse(ptr));
 	}
 
 	public boolean equals(Object o)        
@@ -127,8 +137,14 @@ public class JDDNode
 	 */
 	public JDDNode copy()
 	{
-		JDD.Ref(this);
-		return new JDDNode(this);
+		JDDNode result;
+		if (DebugJDD.debugEnabled) {
+			result = new DebugJDD.DebugJDDNode(ptr, false);
+		} else {
+			result = new JDDNode(ptr());
+		}
+		JDD.Ref(result);
+		return result;
 	}
 }