diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index 02e7d3f6..b7139e88 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -1054,7 +1054,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkRewardPathFormula(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
-		if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){
+		if (Expression.isReach(expr)) {
 			return checkRewardReach(model, modelRewards, (ExpressionTemporal) expr, minMax, statesOfInterest);
 		}
 		else if (Expression.isCoSafeLTLSyntactic(expr)) {
diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index 4366f233..cb770909 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -702,6 +702,19 @@ public abstract class Expression extends ASTElement
 		return false;
 	}
 
+	/**
+	 * Test if an expression is a reachability path formula (F phi) 
+	 */
+	public static boolean isReach(Expression expr)
+	{
+		if (expr instanceof ExpressionTemporal) {
+			if (((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F) {
+				return ((ExpressionTemporal) expr).getOperand2().isProposition();
+			}
+		}
+		return false;
+	}
+
 	/**
 	 * Test if an expression contains time bounds on temporal operators 
 	 */
diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index 1db0630f..e3704be7 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -1186,7 +1186,7 @@ public class NondetModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
 	{
-		if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){
+		if (Expression.isReach(expr)) {
 			return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min);
 		}
 		else if (Expression.isCoSafeLTLSyntactic(expr)) {