diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java
index f5b5d459..81fe13e3 100644
--- a/prism/src/explicit/ConstructModel.java
+++ b/prism/src/explicit/ConstructModel.java
@@ -163,15 +163,19 @@ public class ConstructModel extends PrismComponent
 			switch (modelType) {
 			case DTMC:
 				modelSimple = dtmc = new DTMCSimple();
+				dtmc.setVarList(varList);
 				break;
 			case CTMC:
 				modelSimple = ctmc = new CTMCSimple();
+				ctmc.setVarList(varList);
 				break;
 			case MDP:
 				modelSimple = mdp = new MDPSimple();
+				mdp.setVarList(varList);
 				break;
 			case CTMDP:
 				modelSimple = ctmdp = new CTMDPSimple();
+				ctmdp.setVarList(varList);
 				break;
 			case STPG:
 			case SMG:
diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java
index 79626f87..9d618598 100644
--- a/prism/src/explicit/Model.java
+++ b/prism/src/explicit/Model.java
@@ -113,7 +113,10 @@ public interface Model
 	 * Get access to a list of states (optionally stored).
 	 */
 	public List<State> getStatesList();
-	
+
+	/** Get access to the VarList (optionally stored) */
+	public VarList getVarList();
+
 	/**
 	 * Get access to a list of constant values (optionally stored).
 	 */
diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java
index dfda6bd0..8d6698a7 100644
--- a/prism/src/explicit/ModelExplicit.java
+++ b/prism/src/explicit/ModelExplicit.java
@@ -66,6 +66,8 @@ public abstract class ModelExplicit implements Model
 	protected List<State> statesList;
 	/** (Optionally) a list of values for constants associated with this model. */
 	protected Values constantValues;
+	/** (Optionally) the list of variables */
+	protected VarList varList;
 	/** (Optionally) some labels (atomic propositions) associated with the model,
 	 * represented as a String->BitSet mapping from their names to the states that satisfy them. */
 	protected Map<String, BitSet> labels = new TreeMap<String, BitSet>();
@@ -94,6 +96,7 @@ public abstract class ModelExplicit implements Model
 		statesList = model.statesList;
 		constantValues = model.constantValues;
 		labels = model.labels;
+		varList = model.varList;
 	}
 
 	/**
@@ -117,6 +120,7 @@ public abstract class ModelExplicit implements Model
 		statesList = null;
 		constantValues = model.constantValues;
 		labels.clear();
+		varList = model.varList;
 	}
 
 	/**
@@ -129,6 +133,7 @@ public abstract class ModelExplicit implements Model
 		deadlocks = new TreeSet<Integer>();
 		statesList = null;
 		constantValues = null;
+		varList = null;
 		labels = new TreeMap<String, BitSet>();
 	}
 
@@ -177,6 +182,14 @@ public abstract class ModelExplicit implements Model
 		this.constantValues = constantValues;
 	}
 
+	/**
+	 * Sets the VarList for this model (may be {@code null}).
+	 */
+	public void setVarList(VarList varList)
+	{
+		this.varList = varList;
+	}
+
 	/**
 	 * Adds a label and the set the states that satisfy it.
 	 * Any existing label with the same name is overwritten.
@@ -269,6 +282,12 @@ public abstract class ModelExplicit implements Model
 	{
 		return constantValues;
 	}
+	
+	@Override
+	public VarList getVarList()
+	{
+		return varList;
+	}
 
 	@Override
 	public BitSet getLabelStates(String name)
@@ -469,4 +488,4 @@ public abstract class ModelExplicit implements Model
 		predecessorRelation = null;
 	}
 
-}
\ No newline at end of file
+}
diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java
index f90b2d07..4e547340 100644
--- a/prism/src/explicit/SubNondetModel.java
+++ b/prism/src/explicit/SubNondetModel.java
@@ -173,6 +173,14 @@ public class SubNondetModel implements NondetModel
 		return statesList;
 	}
 
+	@Override
+	public VarList getVarList()
+	{
+		// we can return the varList of the model, as we do not change
+		// the variables in the model
+		return model.getVarList();
+	}
+
 	@Override
 	public Values getConstantValues()
 	{