diff --git a/prism/src/dv/DoubleVector.java b/prism/src/dv/DoubleVector.java
index abec1a8a..1b66e4a2 100644
--- a/prism/src/dv/DoubleVector.java
+++ b/prism/src/dv/DoubleVector.java
@@ -105,11 +105,16 @@ public class DoubleVector
 	/**
 	 * Create a new DoubleVector from an existing MTBDD representation of an array.
 	 * <br>[ DEREFS: <i>none</i> ]
+	 * @throws PrismException if number of states is too large (uses Java int based indices)
 	 */
-	public DoubleVector(JDDNode dd, JDDVars vars, ODDNode odd)
+	public DoubleVector(JDDNode dd, JDDVars vars, ODDNode odd) throws PrismException
 	{
+		long numStates = odd.getEOff() + odd.getTOff();
+		if (numStates > Integer.MAX_VALUE) {
+			throw new PrismNotSupportedException("Can not create DoubleVector with more than " + Integer.MAX_VALUE + " states, have " + numStates + " states");
+		}
 		v = DV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr());
-		n = (int)(odd.getEOff() + odd.getTOff());
+		n = (int)numStates;
 	}
 	
 	private native long DV_ConvertMTBDD(long dd, long vars, int num_vars, long odd);
diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index 3cebbe1c..82289243 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/prism/src/prism/ProbModelChecker.java
@@ -1252,7 +1252,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	 * the (single) initial state or equiprobable over multiple initial states.
 	 * The type of storage (MTBDD or double vector) matches the current engine.
 	 */
-	private StateValues buildInitialDistribution()
+	private StateValues buildInitialDistribution() throws PrismException
 	{
 		StateValues dist = null;
 		JDDNode init;
diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java
index ac4b876f..d7501945 100644
--- a/prism/src/prism/StateValues.java
+++ b/prism/src/prism/StateValues.java
@@ -38,7 +38,7 @@ import parser.ast.RelOp;
 public interface StateValues extends StateVector
 {
 	/** Converts to StateValuesDV, destroys (clear) this vector */
-	StateValuesDV convertToStateValuesDV();
+	StateValuesDV convertToStateValuesDV() throws PrismException;
 
 	/** Converts to StateValuesMTBDD, destroys (clear) this vector */
 	StateValuesMTBDD convertToStateValuesMTBDD();
diff --git a/prism/src/prism/StateValuesDV.java b/prism/src/prism/StateValuesDV.java
index d318a2f4..8fc1aa37 100644
--- a/prism/src/prism/StateValuesDV.java
+++ b/prism/src/prism/StateValuesDV.java
@@ -113,7 +113,7 @@ public class StateValuesDV implements StateValues
 	 * @param dd the double vector
 	 * @param model the underlying model
 	 */
-	public StateValuesDV(JDDNode dd, Model model)
+	public StateValuesDV(JDDNode dd, Model model) throws PrismException
 	{
 		// TODO: Enforce/check that dd is zero for all non-reachable states
 		this(new DoubleVector(dd, model.getAllDDRowVars(), model.getODD()), model);
diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java
index 0a49ac16..b46ef20e 100644
--- a/prism/src/prism/StateValuesMTBDD.java
+++ b/prism/src/prism/StateValuesMTBDD.java
@@ -104,7 +104,7 @@ public class StateValuesMTBDD implements StateValues
 	// CONVERSION METHODS
 	
 	@Override
-	public StateValuesDV convertToStateValuesDV()
+	public StateValuesDV convertToStateValuesDV() throws PrismException
 	{
 		// convert to StateValuesDV, destroy (clear) old vector
 		StateValuesDV res = new StateValuesDV(values, model);