diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java
index 51917514..ff7f36dc 100644
--- a/prism/src/explicit/CTMCModelChecker.java
+++ b/prism/src/explicit/CTMCModelChecker.java
@@ -935,7 +935,7 @@ public class CTMCModelChecker extends ProbModelChecker
 			ctmc.buildFromPrismExplicit(args[0]);
 			ctmc.addInitialState(0);
 			//System.out.println(ctmc);
-			labels = mc.loadLabelsFile(args[1]);
+			labels = StateModelChecker.loadLabelsFile(args[1]);
 			//System.out.println(labels);
 			target = labels.get(args[2]);
 			if (target == null)
diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java
index 53a973ac..e49accfc 100644
--- a/prism/src/explicit/CTMDPModelChecker.java
+++ b/prism/src/explicit/CTMDPModelChecker.java
@@ -286,7 +286,7 @@ public class CTMDPModelChecker extends ProbModelChecker
 			ctmdp.buildFromPrismExplicit(args[0]);
 			ctmdp.addInitialState(0);
 			System.out.println(ctmdp);
-			labels = mc.loadLabelsFile(args[1]);
+			labels = StateModelChecker.loadLabelsFile(args[1]);
 			System.out.println(labels);
 			target = labels.get(args[2]);
 			if (target == null)
diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index d72741f4..28cc2cf6 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -1624,7 +1624,7 @@ public class DTMCModelChecker extends ProbModelChecker
 				dtmc.buildFromPrismExplicit(args[0]);
 				dtmc.addInitialState(0);
 				//System.out.println(dtmc);
-				Map<String, BitSet> labels = mc.loadLabelsFile(args[1]);
+				Map<String, BitSet> labels = StateModelChecker.loadLabelsFile(args[1]);
 				//System.out.println(labels);
 				BitSet target = labels.get(args[2]);
 				if (target == null)
diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index edec0848..b2b1e183 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -1756,7 +1756,7 @@ public class MDPModelChecker extends ProbModelChecker
 			mdp.buildFromPrismExplicit(args[0]);
 			mdp.addInitialState(0);
 			//System.out.println(mdp);
-			labels = mc.loadLabelsFile(args[1]);
+			labels = StateModelChecker.loadLabelsFile(args[1]);
 			//System.out.println(labels);
 			init = labels.get("init");
 			target = labels.get(args[2]);
diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java
index 88a3ace6..02ba0805 100644
--- a/prism/src/explicit/PrismSTPGAbstractRefine.java
+++ b/prism/src/explicit/PrismSTPGAbstractRefine.java
@@ -116,8 +116,9 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 			}
 		}
 
+		new StateModelChecker(null);
 		// Get initial/target (concrete) states
-		labels = new StateModelChecker(null).loadLabelsFile(labFile);
+		labels = StateModelChecker.loadLabelsFile(labFile);
 		initialConcrete = labels.get("init");
 		targetConcrete = labels.get(targetLabel);
 		if (targetConcrete == null)
diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java
index b5fce8d8..2e1bc463 100644
--- a/prism/src/explicit/STPGModelChecker.java
+++ b/prism/src/explicit/STPGModelChecker.java
@@ -920,7 +920,7 @@ public class STPGModelChecker extends ProbModelChecker
 			stpg.buildFromPrismExplicit(args[0]);
 			stpg.addInitialState(0);
 			//System.out.println(stpg);
-			labels = mc.loadLabelsFile(args[1]);
+			labels = StateModelChecker.loadLabelsFile(args[1]);
 			//System.out.println(labels);
 			target = labels.get(args[2]);
 			if (target == null)