diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index 836df459..7206f34b 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -248,18 +248,19 @@ public class DTMCModelChecker extends ProbModelChecker
 		modelProduct = pair.first;
 		int invMap[] = pair.second;
 		int modelProductSize = modelProduct.getNumStates();
+		mainLog.print("\n" + modelProduct.infoStringTable());
+		mainLog.print(modelProduct);
 
 		// Find accepting BSCCs + compute reachability probabilities
 		mainLog.println("\nFinding accepting BSCCs...");
 		BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCs(dra, modelProduct, invMap, sccMethod);
-		mainLog.println(acceptingBSCCs);
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new DTMCModelChecker();
 		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct);
 
 		// Mapping probabilities in the original model
 		double[] probsProductDbl = probsProduct.getDoubleArray();
-		double[] probsDbl = new double[modelProductSize];
+		double[] probsDbl = new double[model.getNumStates()];
 
 		LinkedList<Integer> queue = new LinkedList<Integer>();
 		for (int s : model.getInitialStates())