diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index dd36a0e2..dc1ba773 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/prism/src/prism/LTLModelChecker.java
@@ -236,10 +236,8 @@ public class LTLModelChecker extends PrismComponent
 			before = false;
 		}
 
-		// If passed in var lists are null, create new lists
-		// (which won't be accessible later in this case)
-		daDDRowVars = (daDDRowVarsCopy == null) ? new JDDVars() : daDDRowVarsCopy;
-		daDDColVars = (daDDColVarsCopy == null) ? new JDDVars() : daDDColVarsCopy;
+		daDDRowVars = new JDDVars();
+		daDDColVars = new JDDVars();
 		// Create the new dd variables
 		newDDVarNames = new Vector<String>();
 		newDDVarNames.addAll(ddVarNames);
@@ -295,6 +293,8 @@ public class LTLModelChecker extends PrismComponent
 		}
 		daDDRowVars.refAll();
 		daDDColVars.refAll();
+		daDDRowVars.refAll();
+		daDDColVars.refAll();
 
 		// Build transition matrix for product
 		newTrans = buildTransMask(da, labelDDs, allDDRowVars, allDDColVars, daDDRowVars, daDDColVars);
@@ -345,11 +345,14 @@ public class LTLModelChecker extends PrismComponent
 		newStart = JDD.And(model.getStart(), newStart);
 		modelProd.setStart(newStart);
 
-		// Reference DA DD vars (if being returned)
+		// if possible, return copies of the DA DD variables via the method parameters
 		if (daDDRowVarsCopy != null)
-			daDDRowVarsCopy.refAll();
+			daDDRowVarsCopy.copyVarsFrom(daDDRowVars);
 		if (daDDColVarsCopy != null)
-			daDDColVarsCopy.refAll();
+			daDDColVarsCopy.copyVarsFrom(daDDColVars);
+
+		daDDRowVars.derefAll();
+		daDDColVars.derefAll();
 
 		return modelProd;
 	}