diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java
index 848551cb..3aece49a 100644
--- a/prism/src/parser/ast/ExpressionFunc.java
+++ b/prism/src/parser/ast/ExpressionFunc.java
@@ -232,12 +232,20 @@ public class ExpressionFunc extends Expression
 
 	public Object evaluateFloor(EvaluateContext ec) throws PrismLangException
 	{
-		return new Integer((int) Math.floor(getOperand(0).evaluateDouble(ec)));
+		double d = Math.floor(getOperand(0).evaluateDouble(ec));
+		// Check for NaN or +/-inf, otherwise possible errors lost in cast to int
+		if (Double.isNaN(d) || Double.isInfinite(d))
+			throw new PrismLangException("Cannot take floor() of " + d, this);
+		return new Integer((int) d);
 	}
 
 	public Object evaluateCeil(EvaluateContext ec) throws PrismLangException
 	{
-		return new Integer((int) Math.ceil(getOperand(0).evaluateDouble(ec)));
+		double d = Math.ceil(getOperand(0).evaluateDouble(ec));
+		// Check for NaN or +/-inf, otherwise possible errors lost in cast to int
+		if (Double.isNaN(d) || Double.isInfinite(d))
+			throw new PrismLangException("Cannot take ceil() of " + d, this);
+		return new Integer((int) d);
 	}
 
 	public Object evaluatePow(EvaluateContext ec) throws PrismLangException
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index d53f2a0e..53e07083 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -781,9 +781,11 @@ public class StateModelChecker implements ModelChecker
 			dd1 = ((StateValuesMTBDD) res1).getJDDNode();
 			switch (op) {
 			case ExpressionFunc.FLOOR:
+				// NB: Floor result kept as double, so don't need to check if operand is NaN
 				dd1 = JDD.MonadicApply(JDD.FLOOR, dd1);
 				break;
 			case ExpressionFunc.CEIL:
+				// NB: Ceil result kept as double, so don't need to check if operand is NaN
 				dd1 = JDD.MonadicApply(JDD.CEIL, dd1);
 				break;
 			}
@@ -795,10 +797,12 @@ public class StateModelChecker implements ModelChecker
 			n = dv1.getSize();
 			switch (op) {
 			case ExpressionFunc.FLOOR:
+				// NB: Floor result kept as double, so don't need to check if operand is NaN
 				for (i = 0; i < n; i++)
 					dv1.setElement(i, Math.floor(dv1.getElement(i)));
 				break;
 			case ExpressionFunc.CEIL:
+				// NB: Ceil result kept as double, so don't need to check if operand is NaN
 				for (i = 0; i < n; i++)
 					dv1.setElement(i, Math.ceil(dv1.getElement(i)));
 				break;