diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index 5fb332e2..43f7d636 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -487,7 +487,9 @@ public class NondetModelChecker extends NonProbModelChecker
 		// First, filter over DRA start states
 		// (which we can get from initial states of product model,
 		// because of the way it is constructed)
-		startMask = modelProduct.getStart();
+		startMask = mcLtl.buildStartMask(dra, labelDDs, draDDRowVars);
+		JDD.Ref(model.getReach());
+		startMask = JDD.And(model.getReach(), startMask);
 		probsProduct.filter(startMask);
 		// Then sum over DD vars for the DRA state
 		probs = probsProduct.sumOverDDVars(draDDRowVars, model);
@@ -499,6 +501,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			JDD.Deref(labelDDs.get(i));
 		}
 		JDD.Deref(acc);
+		JDD.Deref(startMask);
 		draDDRowVars.derefAll();
 		draDDColVars.derefAll();
 
diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index d87363dd..3192cb21 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/prism/src/prism/ProbModelChecker.java
@@ -648,9 +648,9 @@ public class ProbModelChecker extends NonProbModelChecker
 		
 		// Convert probability vector to original model
 		// First, filter over DRA start states
-		// (which we can get from initial states of product model,
-		// because of the way it is constructed)
-		startMask = modelProduct.getStart();
+		startMask = mcLtl.buildStartMask(dra, labelDDs, draDDRowVars);
+		JDD.Ref(model.getReach());
+		startMask = JDD.And(model.getReach(), startMask);
 		probsProduct.filter(startMask);
 		// Then sum over DD vars for the DRA state
 		probs = probsProduct.sumOverDDVars(draDDRowVars, model);
@@ -662,6 +662,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			JDD.Deref(labelDDs.get(i));
 		}
 		JDD.Deref(acc);
+		JDD.Deref(startMask);
 		draDDRowVars.derefAll();
 		draDDColVars.derefAll();