diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index f760cf57..2e1eeefe 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/prism/src/explicit/StateModelChecker.java
@@ -844,6 +844,10 @@ public class StateModelChecker extends PrismComponent
 		} else {
 			currentFilter = null;
 		}
+		if (op == FilterOperator.FIRST) {
+			// only first state is of interest
+			bsFilter.clear(bsFilter.nextSetBit(0) + 1, bsFilter.length());
+		}
 
 		// Check operand recursively, using bsFilter as statesOfInterest
 		StateValues vals = checkExpression(model, expr.getOperand(), bsFilter);
diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java
index aff8ca34..dddd10e1 100644
--- a/prism/src/param/ParamModelChecker.java
+++ b/prism/src/param/ParamModelChecker.java
@@ -511,6 +511,10 @@ final public class ParamModelChecker extends PrismComponent
 			s += " (but \"" + filter + "\" is true in " + bsFilter.cardinality() + " states)";
 			throw new PrismException(s);
 		}
+		if (op == FilterOperator.FIRST) {
+			// only first state is of interest
+			bsFilter.clear(bsFilter.nextSetBit(0) + 1, bsFilter.length());
+		}
 		RegionValues vals = checkExpression(model, expr.getOperand(), bsFilter);
 
 		// Check if filter state set is empty; we treat this as an error