diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index af527b32..fd70ca4d 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -890,9 +890,6 @@ public class ProbModelChecker extends NonProbModelChecker
 		if (expr.getType() instanceof TypePathDouble) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			switch (exprTemp.getOperator()) {
-			case ExpressionTemporal.R_F:
-				rewards = checkRewardReach(model, modelRewards, exprTemp, minMax, statesOfInterest);
-				break;
 			case ExpressionTemporal.R_I:
 				rewards = checkRewardInstantaneous(model, modelRewards, exprTemp, minMax);
 				break;
diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java
index 0e28ffe9..90e09ee8 100644
--- a/prism/src/param/ParamModelChecker.java
+++ b/prism/src/param/ParamModelChecker.java
@@ -1007,7 +1007,7 @@ final public class ParamModelChecker extends PrismComponent
 		if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			switch (exprTemp.getOperator()) {
-			case ExpressionTemporal.R_F:
+			case ExpressionTemporal.P_F:
 				rewards = checkRewardReach(model, rew, exprTemp, min, needStates);
 				break;
 			case ExpressionTemporal.R_S:
diff --git a/prism/src/parser/visitor/SemanticCheck.java b/prism/src/parser/visitor/SemanticCheck.java
index fd84296a..59e4320c 100644
--- a/prism/src/parser/visitor/SemanticCheck.java
+++ b/prism/src/parser/visitor/SemanticCheck.java
@@ -384,9 +384,6 @@ public class SemanticCheck extends ASTTraverse
 		if (op == ExpressionTemporal.R_I && (operand1 != null || operand2 != null || lBound != null || uBound == null)) {
 			throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e);
 		}
-		if (op == ExpressionTemporal.R_F && (operand1 != null || operand2 == null || lBound != null || uBound != null)) {
-			throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e);
-		}
 		if (op == ExpressionTemporal.R_S && (operand1 != null || operand2 != null || lBound != null || uBound != null)) {
 			throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e);
 		}
diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java
index 98e28ae8..b5139f66 100644
--- a/prism/src/parser/visitor/TypeCheck.java
+++ b/prism/src/parser/visitor/TypeCheck.java
@@ -193,14 +193,6 @@ public class TypeCheck extends ASTTraverse
 			}
 			e.setType(TypePathBool.getInstance());
 			break;
-		case ExpressionTemporal.R_F:
-			if (e.getOperand2() != null) {
-				type = e.getOperand2().getType();
-				if (!(type instanceof TypeBool) && !(type instanceof TypePathBool))
-					throw new PrismLangException("Type error: Argument of " + e.getOperatorSymbol() + " operator is not Boolean", e.getOperand2());
-			}
-			e.setType(TypePathDouble.getInstance());
-			break;
 		case ExpressionTemporal.R_C:
 		case ExpressionTemporal.R_I:
 		case ExpressionTemporal.R_S:
diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index b3a22764..ca9d4b38 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -249,9 +249,6 @@ public class NondetModelChecker extends NonProbModelChecker
 			case ExpressionTemporal.R_I:
 				rewards = checkRewardInst(exprTemp, stateRewards, transRewards, minMax.isMin());
 				break;
-			case ExpressionTemporal.R_F:
-				rewards = checkRewardReach(exprTemp, stateRewards, transRewards, minMax.isMin());
-				break;
 			}
 		} else if (expr2.getType() instanceof TypePathBool || expr2.getType() instanceof TypeBool) {
 			rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, minMax.isMin());
diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index f2e98250..40bca11a 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/prism/src/prism/ProbModelChecker.java
@@ -237,9 +237,6 @@ public class ProbModelChecker extends NonProbModelChecker
 			case ExpressionTemporal.R_I:
 				rewards = checkRewardInst(exprTemp, stateRewards, transRewards);
 				break;
-			case ExpressionTemporal.R_F:
-				rewards = checkRewardReach(exprTemp, stateRewards, transRewards);
-				break;
 			case ExpressionTemporal.R_S:
 				rewards = checkRewardSS(exprTemp, stateRewards, transRewards);
 				break;
diff --git a/prism/src/simulator/sampler/Sampler.java b/prism/src/simulator/sampler/Sampler.java
index e10212f0..469ad151 100644
--- a/prism/src/simulator/sampler/Sampler.java
+++ b/prism/src/simulator/sampler/Sampler.java
@@ -253,7 +253,7 @@ public abstract class Sampler
 				// Discrete-time instantaneous reward
 				return new SamplerRewardInstDisc(exprTemp, rsi);
 			}
-		case ExpressionTemporal.R_F:
+		case ExpressionTemporal.P_F:
 			// reachability reward
 			return new SamplerRewardReach(exprTemp, rsi);
 		}
diff --git a/prism/src/simulator/sampler/SamplerRewardReach.java b/prism/src/simulator/sampler/SamplerRewardReach.java
index a8cec7e9..5eec550a 100644
--- a/prism/src/simulator/sampler/SamplerRewardReach.java
+++ b/prism/src/simulator/sampler/SamplerRewardReach.java
@@ -49,7 +49,7 @@ public class SamplerRewardReach extends SamplerDouble
 		
 		// Make sure expression is of the correct type
 		// Then extract other required info
-		if (expr.getOperator() != ExpressionTemporal.R_F)
+		if (expr.getOperator() != ExpressionTemporal.P_F)
 			throw new PrismException("Error creating Sampler");
 		target = expr.getOperand2();
 		this.rewardStructIndex = rewardStructIndex;