diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java
index 1292f2ef..c5768926 100644
--- a/prism/src/prism/Modules2MTBDD.java
+++ b/prism/src/prism/Modules2MTBDD.java
@@ -310,32 +310,20 @@ public class Modules2MTBDD
 		// deref spare dds
 		globalDDRowVars.derefAll();
 		globalDDColVars.derefAll();
-		for (i = 0; i < numModules; i++) {
-			JDD.Deref(moduleIdentities[i]);
-			JDD.Deref(moduleRangeDDs[i]);
-		}
-		for (i = 0; i < numVars; i++) {
-			JDD.Deref(varIdentities[i]);
-			JDD.Deref(varRangeDDs[i]);
-			JDD.Deref(varColRangeDDs[i]);
-		}
+		JDD.DerefArray(moduleIdentities, numModules);
+		JDD.DerefArray(moduleRangeDDs, numModules);
+		JDD.DerefArray(varIdentities, numVars);
+		JDD.DerefArray(varRangeDDs, numVars);
+		JDD.DerefArray(varColRangeDDs, numVars);
 		JDD.Deref(range);
 		if (modelType == ModelType.MDP) {
-			for (i = 0; i < ddSynchVars.length; i++) {
-				JDD.Deref(ddSynchVars[i]);
-			}
-			for (i = 0; i < ddSchedVars.length; i++) {
-				JDD.Deref(ddSchedVars[i]);
-			}
-			for (i = 0; i < ddChoiceVars.length; i++) {
-				JDD.Deref(ddChoiceVars[i]);
-			}
+			JDD.DerefArray(ddSynchVars, ddSynchVars.length);
+			JDD.DerefArray(ddSchedVars, ddSchedVars.length);
+			JDD.DerefArray(ddChoiceVars, ddChoiceVars.length);
 		}
 		if (doSymmetry) {
 			JDD.Deref(symm);
-			for (i = 0; i < numSymmModules-1; i++) {
-				JDD.Deref(nonSymms[i]);
-			}
+			JDD.DerefArray(nonSymms, numSymmModules-1);
 		}
 		
 		expr2mtbdd.clearDummyModel();
@@ -598,26 +586,20 @@ public class Modules2MTBDD
 			// go thru all syncronising action vars
 			for (i = 0; i < ddSynchVars.length; i++) {
 				// add to list
-				JDD.Ref(ddSynchVars[i]);
-				JDD.Ref(ddSynchVars[i]);
-				allDDSynchVars.addVar(ddSynchVars[i]);
-				allDDNondetVars.addVar(ddSynchVars[i]);
+				allDDSynchVars.addVar(ddSynchVars[i].copy());
+				allDDNondetVars.addVar(ddSynchVars[i].copy());
 			}
 			// go thru all scheduler nondet vars
 			for (i = 0; i < ddSchedVars.length; i++) {
 				// add to list
-				JDD.Ref(ddSchedVars[i]);
-				JDD.Ref(ddSchedVars[i]);
-				allDDSchedVars.addVar(ddSchedVars[i]);
-				allDDNondetVars.addVar(ddSchedVars[i]);
+				allDDSchedVars.addVar(ddSchedVars[i].copy());
+				allDDNondetVars.addVar(ddSchedVars[i].copy());
 			}
 			// go thru all local nondet vars
 			for (i = 0; i < ddChoiceVars.length; i++) {
 				// add to list
-				JDD.Ref(ddChoiceVars[i]);
-				JDD.Ref(ddChoiceVars[i]);
-				allDDChoiceVars.addVar(ddChoiceVars[i]);
-				allDDNondetVars.addVar(ddChoiceVars[i]);
+				allDDChoiceVars.addVar(ddChoiceVars[i].copy());
+				allDDNondetVars.addVar(ddChoiceVars[i].copy());
 			}
 		}
 	}
@@ -646,8 +628,7 @@ public class Modules2MTBDD
 			id = JDD.Constant(1);
 			for (j = 0; j < numVars; j++) {
 				if (varList.getModule(j) == i) {
-					JDD.Ref(varIdentities[j]);
-					id = JDD.Apply(JDD.TIMES, id, varIdentities[j]);
+					id = JDD.Apply(JDD.TIMES, id, varIdentities[j].copy());
 				}
 			}
 			moduleIdentities[i] = id;
@@ -668,21 +649,17 @@ public class Modules2MTBDD
 		varColRangeDDs = new JDDNode[numVars];
 		for (i = 0; i < numVars; i++) {
 			// obtain range dd by abstracting from identity matrix
-			JDD.Ref(varIdentities[i]);
-			varRangeDDs[i] = JDD.SumAbstract(varIdentities[i], varDDColVars[i]);
+			varRangeDDs[i] = JDD.SumAbstract(varIdentities[i].copy(), varDDColVars[i]);
 			// obtain range dd by abstracting from identity matrix
-			JDD.Ref(varIdentities[i]);
-			varColRangeDDs[i] = JDD.SumAbstract(varIdentities[i], varDDRowVars[i]);
+			varColRangeDDs[i] = JDD.SumAbstract(varIdentities[i].copy(), varDDRowVars[i]);
 			// build up range for whole system as we go
-			JDD.Ref(varRangeDDs[i]);
-			range = JDD.Apply(JDD.TIMES, range, varRangeDDs[i]);
+			range = JDD.Apply(JDD.TIMES, range, varRangeDDs[i].copy());
 		}
 		// module ranges
 		moduleRangeDDs = new JDDNode[numModules];
 		for (i = 0; i < numModules; i++) {
 			// obtain range dd by abstracting from identity matrix
-			JDD.Ref(moduleIdentities[i]);
-			moduleRangeDDs[i] = JDD.SumAbstract(moduleIdentities[i], moduleDDColVars[i]);			
+			moduleRangeDDs[i] = JDD.SumAbstract(moduleIdentities[i].copy(), moduleDDColVars[i]);
 		}
 	}
 
@@ -715,8 +692,7 @@ public class Modules2MTBDD
 		// for dtmcs, need to normalise each row to remove local nondeterminism
 		if (modelType == ModelType.DTMC) {
 			// divide each row by row sum
-			JDD.Ref(trans);
-			tmp = JDD.SumAbstract(trans, allDDColVars);
+			tmp = JDD.SumAbstract(trans.copy(), allDDColVars);
 			trans = JDD.Apply(JDD.DIVIDE, trans, tmp);
 		}
 	}
@@ -783,8 +759,7 @@ public class Modules2MTBDD
 			// independent bit
 			tmp = JDD.Constant(1);
 			for (i = 0; i < numSynchs; i++) {
-				JDD.Ref(ddSynchVars[i]);
-				tmp = JDD.And(tmp, JDD.Not(ddSynchVars[i]));
+				tmp = JDD.And(tmp, JDD.Not(ddSynchVars[i].copy()));
 			}
 			sysDDs.ind.trans = JDD.Apply(JDD.TIMES, tmp, sysDDs.ind.trans);
 			//JDD.Ref(tmp);
@@ -793,12 +768,11 @@ public class Modules2MTBDD
 			for (i = 0; i < numSynchs; i++) {
 				tmp = JDD.Constant(1);
 				for (j = 0; j < numSynchs; j++) {
-					JDD.Ref(ddSynchVars[j]);
 					if (j == i) {
-						tmp = JDD.And(tmp, ddSynchVars[j]);
+						tmp = JDD.And(tmp, ddSynchVars[j].copy());
 					}
 					else {
-						tmp = JDD.And(tmp, JDD.Not(ddSynchVars[j]));
+						tmp = JDD.And(tmp, JDD.Not(ddSynchVars[j].copy()));
 					}
 				}
 				sysDDs.synchs[i].trans = JDD.Apply(JDD.TIMES, tmp, sysDDs.synchs[i].trans);
@@ -813,14 +787,12 @@ public class Modules2MTBDD
 		// now, for all model types, transition matrix can be built by summing over all actions
 		// also build transition rewards at the same time
 		n = modulesFile.getNumRewardStructs();
-		JDD.Ref(sysDDs.ind.trans);
-		trans = sysDDs.ind.trans;
+		trans = sysDDs.ind.trans.copy();
 		for (j = 0; j < n; j++) {
 			transRewards[j] = sysDDs.ind.rewards[j];
 		}
 		for (i = 0; i < numSynchs; i++) {
-			JDD.Ref(sysDDs.synchs[i].trans);
-			trans = JDD.Apply(JDD.PLUS, trans, sysDDs.synchs[i].trans);
+			trans = JDD.Apply(JDD.PLUS, trans, sysDDs.synchs[i].trans.copy());
 			for (j = 0; j < n; j++) {
 				transRewards[j] = JDD.Apply(JDD.PLUS, transRewards[j], sysDDs.synchs[i].rewards[j]);
 			}
@@ -833,20 +805,17 @@ public class Modules2MTBDD
 		if (modelType != ModelType.MDP) {
 			n = modulesFile.getNumRewardStructs();
 			for (j = 0; j < n; j++) {
-				JDD.Ref(trans);
-				transRewards[j] = JDD.Apply(JDD.DIVIDE, transRewards[j], trans);
+				transRewards[j] = JDD.Apply(JDD.DIVIDE, transRewards[j], trans.copy());
 			}
 		}
 		
 		// For MDPs, we take a copy of the DDs used to construct the part
 		// of the transition matrix that corresponds to each action
 		if (modelType == ModelType.MDP && storeTransParts) {
-			JDD.Ref(sysDDs.ind.trans);
-			transInd = JDD.ThereExists(JDD.GreaterThan(sysDDs.ind.trans, 0), allDDColVars);
+			transInd = JDD.ThereExists(JDD.GreaterThan(sysDDs.ind.trans.copy(), 0), allDDColVars);
 			transSynch = new JDDNode[numSynchs];
 			for (i = 0; i < numSynchs; i++) {
-				JDD.Ref(sysDDs.synchs[i].trans);
-				transSynch[i] = JDD.ThereExists(JDD.GreaterThan(sysDDs.synchs[i].trans, 0), allDDColVars);
+				transSynch[i] = JDD.ThereExists(JDD.GreaterThan(sysDDs.synchs[i].trans.copy(), 0), allDDColVars);
 			}
 		}
 		
@@ -874,8 +843,7 @@ public class Modules2MTBDD
 				//tmp = JDD.ThereExists(JDD.GreaterThan(sysDDs.ind.trans, 0), allDDColVars);
 				//transActions = JDD.Apply(JDD.PLUS, transActions, JDD.Apply(JDD.TIMES, tmp, JDD.Constant(1)));
 				for (i = 0; i < numSynchs; i++) {
-					JDD.Ref(sysDDs.synchs[i].trans);
-					tmp = JDD.ThereExists(JDD.GreaterThan(sysDDs.synchs[i].trans, 0), allDDColVars);
+					tmp = JDD.ThereExists(JDD.GreaterThan(sysDDs.synchs[i].trans.copy(), 0), allDDColVars);
 					transActions = JDD.Apply(JDD.PLUS, transActions, JDD.Apply(JDD.TIMES, tmp, JDD.Constant(1+i)));
 				}
 				break;
@@ -883,11 +851,9 @@ public class Modules2MTBDD
 			case CTMC:
 				// Just reference DDs and copy them to new array
 				transPerAction = new JDDNode[numSynchs + 1];
-				JDD.Ref(sysDDs.ind.trans);
-				transPerAction[0] = sysDDs.ind.trans;
+				transPerAction[0] = sysDDs.ind.trans.copy();
 				for (i = 0; i < numSynchs; i++) {
-					JDD.Ref(sysDDs.synchs[i].trans);
-					transPerAction[i + 1] = sysDDs.synchs[i].trans;
+					transPerAction[i + 1] = sysDDs.synchs[i].trans.copy();
 				}
 				break;
 			}
@@ -970,8 +936,7 @@ public class Modules2MTBDD
 			sysDDs.synchs[i] = translateModule(m, module, synch, synchMin[i]);
 		}
 		// store identity matrix
-		JDD.Ref(moduleIdentities[m]);
-		sysDDs.id = moduleIdentities[m];
+		sysDDs.id = moduleIdentities[m].copy();
 		
 		// store synchs used
 		sysDDs.allSynchs.addAll(module.getAllSynchs());
@@ -1568,11 +1533,9 @@ public class Modules2MTBDD
 		}
 		
 		// deref guards/updates
-		for (l = 0; l < numCommands; l++) {
-			JDD.Deref(guardDDs[l]);
-			JDD.Deref(upDDs[l]);
-			//JDD.Deref(rewDDs[l]);
-		}
+		JDD.DerefArray(guardDDs, numCommands);
+		JDD.DerefArray(upDDs, numCommands);
+		//JDD.DerefArray(rewDDs, numCommands);
 		
 		return compDDs;
 	}