diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism b/prism-tests/bugfixes/filters+statesOfInterest.prism
new file mode 100644
index 00000000..c0d80eae
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism
@@ -0,0 +1,23 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+	
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> (s'=7);
+	
+endmodule
+
+rewards "coin_flips"
+	[] s<7 : 1;
+endrewards
diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism.args b/prism-tests/bugfixes/filters+statesOfInterest.prism.args
new file mode 100644
index 00000000..031d5fa5
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism.args
@@ -0,0 +1,4 @@
+-ex
+-m
+-s
+-h
diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism.props b/prism-tests/bugfixes/filters+statesOfInterest.prism.props
new file mode 100644
index 00000000..0ebdee0c
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism.props
@@ -0,0 +1,5 @@
+// Bug fix test case for filters; see commit for details
+// The "0.0+" is needed because of missing integer-valued vector export
+
+// RESULT: 13
+0.0 + filter(sum, filter(count, true, P>0[ X F s=7]), s=2);
diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism.props.args b/prism-tests/bugfixes/filters+statesOfInterest.prism.props.args
new file mode 100644
index 00000000..23ce11d9
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism.props.args
@@ -0,0 +1 @@
+-exportvector filters+statesOfInterest.prism.props.txt
diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism.props.txt b/prism-tests/bugfixes/filters+statesOfInterest.prism.props.txt
new file mode 100644
index 00000000..7a2a6932
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism.props.txt
@@ -0,0 +1,13 @@
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index b19bee4f..aa3b4de8 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -1140,7 +1140,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		boolean filterTrue = Expression.isTrue(filter);
 		// Store some more info
 		String filterStatesString = filterTrue ? "all states" : "states satisfying filter";
-		JDDNode ddFilter = checkExpressionDD(filter, statesOfInterest.copy());
+		JDDNode ddFilter = checkExpressionDD(filter,  model.getReach().copy());
 		StateListMTBDD statesFilter = new StateListMTBDD(ddFilter, model);
 		// Check if filter state set is empty; we treat this as an error
 		if (ddFilter.equals(JDD.ZERO)) {