diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java
index 6a3c7256..3b5ea157 100644
--- a/prism/src/prism/MultiObjModelChecker.java
+++ b/prism/src/prism/MultiObjModelChecker.java
@@ -103,7 +103,7 @@ public class MultiObjModelChecker extends PrismComponent
 		// Build product of MDP and automaton
 		mainLog.println("\nConstructing MDP-DRA product...");
 
-		NondetModel modelNew = mcLtl.constructProductMDP(dra[i], model, labelDDs, draDDRowVars, draDDColVars, false, i == 0 ? ddStateIndex : model.getStart());
+		NondetModel modelNew = mcLtl.constructProductMDP(dra[i], model, labelDDs, draDDRowVars, draDDColVars, (i == 0 ? ddStateIndex : model.getStart()).copy());
 
 		modelNew.printTransInfo(mainLog, prism.getExtraDDInfo());
 		// Deref label BDDs
diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index f67fea25..1d1a5e22 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -1200,9 +1200,6 @@ public class NondetModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
-		// currently, ignore statesOfInterest
-		JDD.Deref(statesOfInterest);
-
 		// For min probabilities, need to negate the formula
 		// (But check fairness setting since this may affect min/max)
 		// (add parentheses to allow re-parsing if required)
@@ -1225,14 +1222,19 @@ public class NondetModelChecker extends NonProbModelChecker
 				AcceptanceType.GENERALIZED_RABIN,
 				AcceptanceType.REACH
 		};
-		da = mcLtl.constructDAForLTLFormula(this, model, expr, labelDDs, allowedAcceptance);
+		try {
+			da = mcLtl.constructDAForLTLFormula(this, model, expr, labelDDs, allowedAcceptance);
+		} catch (Exception e) {
+			JDD.Deref(statesOfInterest);
+			throw e;
+		}
 
 		// Build product of MDP and automaton
 		l = System.currentTimeMillis();
 		mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product...");
 		daDDRowVars = new JDDVars();
 		daDDColVars = new JDDVars();
-		modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars);
+		modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest);
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for product construction: " + l / 1000.0 + " seconds.");
 		mainLog.println();
@@ -1458,9 +1460,6 @@ public class NondetModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
-		// currently, ignore statesOfInterest
-		JDD.Deref(statesOfInterest);
-
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
@@ -1518,7 +1517,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		daDDRowVars = new JDDVars();
 		daDDColVars = new JDDVars();
 		l = System.currentTimeMillis();
-		modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars);
+		modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest);
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for product construction: " + l / 1000.0 + " seconds.");
 		mainLog.println();
diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index 17cde16c..c8982acb 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/prism/src/prism/ProbModelChecker.java
@@ -552,9 +552,6 @@ public class ProbModelChecker extends NonProbModelChecker
 		JDDVars daDDRowVars, daDDColVars;
 		int i;
 
-		// TODO: take statesOfInterest into account for product construction
-		JDD.Deref(statesOfInterest);
-
 		AcceptanceType[] allowedAcceptance = {
 				AcceptanceType.REACH,
 				AcceptanceType.BUCHI,
@@ -571,7 +568,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product...");
 		daDDRowVars = new JDDVars();
 		daDDColVars = new JDDVars();
-		modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars);
+		modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest);
 		mainLog.println();
 		modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
 		// Output product, if required
@@ -968,9 +965,6 @@ public class ProbModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
-		// currently, ignore statesOfInterest
-		JDD.Deref(statesOfInterest);
-
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
@@ -1020,7 +1014,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		daDDRowVars = new JDDVars();
 		daDDColVars = new JDDVars();
 		l = System.currentTimeMillis();
-		modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars);
+		modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest);
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for product construction: " + l / 1000.0 + " seconds.");
 		mainLog.println();