diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index 6a0ff69a..b0ad3e59 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/prism/src/explicit/StateModelChecker.java
@@ -530,8 +530,6 @@ public class StateModelChecker
 
 	protected StateValues checkExpressionFilter(Model model, ExpressionFilter expr) throws PrismException
 	{
-		//throw new PrismException("Explicit engine does not yet handle filters");
-		
 		// Filter info
 		Expression filter;
 		FilterOperator op;
@@ -543,7 +541,6 @@ public class StateModelChecker
 		StateValues vals = null, resVals = null;
 		BitSet bsMatch = null, bs;
 		/*StateListMTBDD states;*/
-		double d = 0.0, d2 = 0.0;
 		boolean b = false;
 		int count = 0;
 		String resultExpl = null;
@@ -620,38 +617,34 @@ public class StateModelChecker
 			bsMatch = vals.getBitSetFromCloseValue(resObj, termCritParam, termCrit == TermCrit.ABSOLUTE);
 			bsMatch.and(bsFilter);
 			break;
-		/*case ARGMIN:
+		case ARGMIN:
 			// Compute/display min
-			d = vals.minOverBDD(bsFilter);
-			mainLog.print("\nMinimum value over " + filterStatesString + ": ");
-			mainLog.println((expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d)));
+			resObj = vals.minOverBitSet(bsFilter);
+			mainLog.print("\nMinimum value over " + filterStatesString + ": " + resObj);
 			// Find states that (are close to) selected value
-			ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
-			JDD.Ref(bsFilter);
-			ddMatch = JDD.And(ddMatch, bsFilter);
+			bsMatch = vals.getBitSetFromCloseValue(resObj, termCritParam, termCrit == TermCrit.ABSOLUTE);
+			bsMatch.and(bsFilter);
 			// Store states in vector; for ARGMIN, don't store a single value (in resObj)
 			// Also, don't bother with explanation string
-			resVals = new StateValuesMTBDD(ddMatch, model);
+			resVals = StateValues.createFromBitSet(bsMatch, model.getNumStates());
 			// Print out number of matching states, but not the actual states
-			mainLog.println("\nNumber of states with minimum value: " + resVals.getNNZString());
-			ddMatch = null;
+			mainLog.println("\nNumber of states with minimum value: " + bsMatch.cardinality());
+			bsMatch = null;
 			break;
 		case ARGMAX:
 			// Compute/display max
-			d = vals.maxOverBDD(bsFilter);
-			mainLog.print("\nMaximum value over " + filterStatesString + ": ");
-			mainLog.println((expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d)));
+			resObj = vals.maxOverBitSet(bsFilter);
+			mainLog.print("\nMaximum value over " + filterStatesString + ": " + resObj);
 			// Find states that (are close to) selected value
-			ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
-			JDD.Ref(bsFilter);
-			ddMatch = JDD.And(ddMatch, bsFilter);
+			bsMatch = vals.getBitSetFromCloseValue(resObj, termCritParam, termCrit == TermCrit.ABSOLUTE);
+			bsMatch.and(bsFilter);
 			// Store states in vector; for ARGMAX, don't store a single value (in resObj)
 			// Also, don't bother with explanation string
-			resVals = new StateValuesMTBDD(ddMatch, model);
+			resVals = StateValues.createFromBitSet(bsMatch, model.getNumStates());
 			// Print out number of matching states, but not the actual states
-			mainLog.println("\nNumber of states with maximum value: " + resVals.getNNZString());
-			ddMatch = null;
-			break;*/
+			mainLog.println("\nNumber of states with maximum value: " + bsMatch.cardinality());
+			bsMatch = null;
+			break;
 		case COUNT:
 			// Compute count
 			count = vals.countOverBitSet(bsFilter);
@@ -662,26 +655,24 @@ public class StateModelChecker
 			resultExpl = filterTrue ? "Count of satisfying states" : "Count of satisfying states also in filter";
 			mainLog.println("\n" + resultExpl + ": " + resObj);
 			break;
-		/*case SUM:
+		case SUM:
 			// Compute sum
-			d = vals.sumOverBDD(bsFilter);
-			// Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion)
-			resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d));
-			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Store as object/vector
+			resObj = vals.sumOverBitSet(bsFilter);
+			resVals = new StateValues(expr.getType(), model.getNumStates(), resObj); 
 			// Create explanation of result and print some details to log
 			resultExpl = "Sum over " + filterStatesString;
 			mainLog.println("\n" + resultExpl + ": " + resObj);
 			break;
 		case AVG:
 			// Compute average
-			d = vals.sumOverBDD(bsFilter) / JDD.GetNumMinterms(bsFilter, allDDRowVars.n());
 			// Store as object/vector
-			resObj = new Double(d);
-			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			resObj = vals.averageOverBitSet(bsFilter);
+			resVals = new StateValues(expr.getType(), model.getNumStates(), resObj); 
 			// Create explanation of result and print some details to log
 			resultExpl = "Average over " + filterStatesString;
 			mainLog.println("\n" + resultExpl + ": " + resObj);
-			break;*/
+			break;
 		case FIRST:
 			// Find first value
 			resObj = vals.firstFromBitSet(bsFilter);
@@ -739,18 +730,14 @@ public class StateModelChecker
 				}
 			}
 			break;
-		/*case EXISTS:
-			// Get access to BDD for this
-			dd = vals.convertToStateValuesMTBDD().getJDDNode();
+		case EXISTS:
+			// Get access to BitSet for this
+			bs = vals.getBitSet();
 			// Check "there exists" over filter
-			JDD.Ref(bsFilter);
-			dd = JDD.And(dd, bsFilter);
-			b = !dd.equals(JDD.ZERO);
+			b = vals.existsOverBitSet(bsFilter);
 			// Store as object/vector
 			resObj = new Boolean(b);
-			resVals = new StateValuesMTBDD(JDD.Constant(b ? 1.0 : 0.0), model);
-			// Set vals to null so that is not clear()-ed twice
-			vals = null;
+			resVals = new StateValues(expr.getType(), model.getNumStates(), resObj); 
 			// Create explanation of result and print some details to log
 			resultExpl = "Property satisfied in ";
 			if (filterTrue) {
@@ -759,9 +746,7 @@ public class StateModelChecker
 				resultExpl += b ? "at least one filter state" : "no filter states";
 			}
 			mainLog.println("\n" + resultExpl);
-			// Derefs
-			JDD.Deref(dd);
-			break;*/
+			break;
 		case STATE:
 			// Check filter satisfied by exactly one state
 			if (bsFilter.cardinality() != 1) {
diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java
index b6bff437..296f5c17 100644
--- a/prism/src/explicit/StateValues.java
+++ b/prism/src/explicit/StateValues.java
@@ -388,18 +388,33 @@ public class StateValues
 	}
 	
 	/**
-	 * Check if true for all states in the (BitSet) filter.
+	 * Check if value is true for all states in the (BitSet) filter.
 	 */
 	public boolean forallOverBitSet(BitSet filter) throws PrismException
 	{
 		if (type instanceof TypeBool) {
 			for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) {
 				if (!valuesB.get(i))
-					return new Boolean(false);
+					return false;
 			}
-			return new Boolean(true);
+			return true;
 		}
-		throw new PrismException("Can't take forall over a vector of type " + type);
+		throw new PrismException("Can't take for-all over a vector of type " + type);
+	}
+	
+	/**
+	 * Check if there exists a true value for some state in the (BitSet) filter.
+	 */
+	public boolean existsOverBitSet(BitSet filter) throws PrismException
+	{
+		if (type instanceof TypeBool) {
+			for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) {
+				if (valuesB.get(i))
+					return true;
+			}
+			return false;
+		}
+		throw new PrismException("Can't take there-exists over a vector of type " + type);
 	}
 	
 	/**
@@ -418,6 +433,48 @@ public class StateValues
 		throw new PrismException("Can't take count over a vector of type " + type);
 	}
 	
+	/**
+	 * Get the sum of values for states that are in the (BitSet) filter.
+	 */
+	public Object sumOverBitSet(BitSet filter) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			int sumI = 0;
+			for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) {
+				sumI += valuesI[i];
+			}
+			return new Integer(sumI);
+		} else if (type instanceof TypeDouble) {
+			double sumD = 0.0;
+			for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) {
+				sumD += valuesD[i];
+			}
+			return new Double(sumD);
+		}
+		throw new PrismException("Can't take sum over a vector of type " + type);
+	}
+	
+	/**
+	 * Get the average of values for states that are in the (BitSet) filter.
+	 */
+	public double averageOverBitSet(BitSet filter) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			int sumI = 0;
+			for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) {
+				sumI += valuesI[i];
+			}
+			return ((double) sumI) / filter.cardinality(); 
+		} else if (type instanceof TypeDouble) {
+			double sumD = 0.0;
+			for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) {
+				sumD += valuesD[i];
+			}
+			return sumD / filter.cardinality(); 
+		}
+		throw new PrismException("Can't take average over a vector of type " + type);
+	}
+	
 	// PRINTING STUFF
 
 	/**