diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index 6bba5df8..88bd59ba 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -41,6 +41,8 @@ import parser.VarList;
 import parser.ast.Declaration;
 import parser.ast.DeclarationIntUnbounded;
 import parser.ast.Expression;
+import parser.ast.ExpressionTemporal;
+import parser.ast.TemporalOperatorBound;
 import prism.AccuracyFactory;
 import prism.ModelType;
 import prism.OptionsIntervalIteration;
diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java
index 2e983124..6ffd2ce2 100644
--- a/prism/src/pta/DigitalClocks.java
+++ b/prism/src/pta/DigitalClocks.java
@@ -721,11 +721,14 @@ public class DigitalClocks
 			// (so just evaluate directly)
 			// We also don't care about the max value - this is done elsewhere;
 			// we just want to make sure that the values is used to compute the GCD
-			if (e.bound.getLowerBound() != null) {
-				allClockVals.add(e.bound.getLowerBound().evaluateInt(constantValues));
-			}
-			if (e.bound.getUpperBound() != null) {
-				allClockVals.add(e.bound.getUpperBound().evaluateInt(constantValues));
+			if (e.getBounds().hasBounds() ) {
+				TemporalOperatorBound bound = e.getBounds().getTimeBoundForContinuousTime();
+				if (bound.getLowerBound() != null) {
+					allClockVals.add(bound.getLowerBound().evaluateInt(constantValues));
+				}
+				if (bound.getUpperBound() != null) {
+					allClockVals.add(bound.getUpperBound().evaluateInt(constantValues));
+				}
 			}
 		}