diff --git a/prism/src/automata/LTL2RabinLibrary.java b/prism/src/automata/LTL2RabinLibrary.java
index 2792ed8a..c8f30ad8 100644
--- a/prism/src/automata/LTL2RabinLibrary.java
+++ b/prism/src/automata/LTL2RabinLibrary.java
@@ -115,24 +115,29 @@ public class LTL2RabinLibrary
 		String draString = dras.get(ltl2.toString());
 		if (draString != null)
 			return createDRAFromString(draString, labels);
-		
-		
+
 		// handle simple until formula with time bounds
 		if (Expression.containsTemporalTimeBounds(ltl)) {
+			if (!ltl.isSimplePathFormula()) {
+				throw new PrismNotSupportedException("Unsupported LTL formula with time bounds: "+ltl);
+			}
+
+			ltl = Expression.convertSimplePathFormulaToCanonicalForm(ltl);
 			boolean negated = false;
-			
+
 			if (ltl instanceof ExpressionUnaryOp &&
 			    ((ExpressionUnaryOp)ltl).getOperator() == ExpressionUnaryOp.NOT) {
 				// negated
 				negated = true;
 				ltl = ((ExpressionUnaryOp)ltl).getOperand();
 			}
-			
+
 			if (ltl instanceof ExpressionTemporal &&
 			    ((ExpressionTemporal)ltl).getOperator() == ExpressionTemporal.P_U) {
 				return constructDRAForSimpleUntilFormula((ExpressionTemporal)ltl, constants, negated);				
 			} else {
-				throw new PrismNotSupportedException("Unsupported LTL formula with time bounds: "+ltl);
+				// should not be reached
+				throw new PrismException("Implementation error");
 			}
 		}
 		
diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java
index 591355f7..11adf611 100644
--- a/prism/src/explicit/LTLModelChecker.java
+++ b/prism/src/explicit/LTLModelChecker.java
@@ -226,15 +226,7 @@ public class LTLModelChecker extends PrismComponent
 				throw new PrismException("Automaton construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
-			if (expr.isSimplePathFormula()) {
-				// Convert simple path formula to canonical form,
-				// DA is then generated by LTL2RabinLibrary.
-				// The conversion to canonical form has to happen here, because once
-				// checkMaximalStateFormulas has been called, the formula should not be modified
-				// anymore, as converters may expect that the generated labels for maximal state
-				// formulas only appear positively
-				expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
-			} else {
+			if (!expr.isSimplePathFormula()) {
 				throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}
diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index f8552cce..58c2af6b 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/prism/src/prism/LTLModelChecker.java
@@ -177,16 +177,7 @@ public class LTLModelChecker extends PrismComponent
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
-			if (expr.isSimplePathFormula()) {
-				// Convert simple path formula to canonical form,
-				// DRA is then generated by LTL2RabinLibrary.
-				//
-				// The conversion to canonical form has to happen here, because once
-				// checkMaximalStateFormulas has been called, the formula should not be modified
-				// anymore, as converters may expect that the generated labels for maximal state
-				// formulas only appear positively
-				expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
-			} else {
+			if (!expr.isSimplePathFormula()) {
 				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}
diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index a6d3355a..3cebbe1c 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/prism/src/prism/ProbModelChecker.java
@@ -880,16 +880,7 @@ public class ProbModelChecker extends NonProbModelChecker
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
-			if (expr.isSimplePathFormula()) {
-				// Convert simple path formula to canonical form,
-				// DA is then generated by LTL2RabinLibrary.
-				//
-				// The conversion to canonical form has to happen here, because once
-				// checkMaximalStateFormulas has been called, the formula should not be modified
-				// anymore, as converters may expect that the generated labels for maximal state
-				// formulas only appear positively
-				expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
-			} else {
+			if (!expr.isSimplePathFormula()) {
 				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}