diff --git a/modules/tlc2/overrides/FiniteSetsExt.java b/modules/tlc2/overrides/FiniteSetsExt.java
index 5b07df5..6afa74e 100644
--- a/modules/tlc2/overrides/FiniteSetsExt.java
+++ b/modules/tlc2/overrides/FiniteSetsExt.java
@@ -38,7 +38,7 @@
 import tlc2.value.impl.KSubsetValue;
 import tlc2.value.impl.OpValue;
 import tlc2.value.impl.SetEnumValue;
-import tlc2.value.impl.SubsetValue;
+import tlc2.value.impl.UserValue;
 import tlc2.value.impl.Value;
 import tlc2.value.impl.ValueEnumeration;
 
@@ -77,23 +77,17 @@ public static Value quantify(final Value set, final OpValue test) {
 	}
 	
 	@TLAPlusOperator(identifier = "kSubset", module = "FiniteSetsExt", warn = false)
-	public static Value kSubset(final Value kv, final Value s) {
-		final SetEnumValue set = (SetEnumValue) s.toSetEnum();
-		if (set == null) {
-			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-					new String[] { "second", "kSubset", "set", Values.ppr(s.toString()) });
-		}
+	public static Value kSubset(final Value kv, final Value set) {
 		if (!(kv instanceof IntValue)) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "first", "kSubset", "natural number", Values.ppr(kv.toString()) });
 		}
 		final int k = ((IntValue) kv).val;
-		
-		if (k < 0 || set.size() < k) {
-			return SetEnumValue.EmptySet;
-		}
-		if (k == 0) {
-			return new SubsetValue(SetEnumValue.EmptySet);
+
+		// Reject non-sets such as 42, TRUE, "foo", <<1>>, [a |-> 1], [x \in {1} |-> x], and model values.
+		if (!(set instanceof Enumerable || set instanceof UserValue)) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "second", "kSubset", "set", Values.ppr(set.toString()) });
 		}
 		return new KSubsetValue(k, set, set.cm);
 	}
diff --git a/tests/FiniteSetsExtTests.tla b/tests/FiniteSetsExtTests.tla
index 26f07a4..05bb62b 100644
--- a/tests/FiniteSetsExtTests.tla
+++ b/tests/FiniteSetsExtTests.tla
@@ -29,29 +29,6 @@ ASSUME LET S == 1..2000000
 
 -----------------------------------------------------------------------------
 
-ASSUME LET S == {"a","b","c","c"} \* Make sure value normalization works.
-       IN \A k \in -1..Cardinality(S) + 1: 
-             kSubset(k, S) = {s \in SUBSET S : Cardinality(s) = k}
-
-ASSUME LET S == {"a","b","c","c"} \* Make sure value normalization works.
-       IN kSubset(-1, S) = {} /\ kSubset(4, S) = {}
-  
-\* The commented variant takes my computer ~30 seconds, whereas the kSubset
-\* variant finishes in under 1s.  
-\*ASSUME LET S == 1..27
-\*       IN {s \in SUBSET S : Cardinality(s) = Cardinality(S)} = {S}
-ASSUME LET S == 1..27
-       IN kSubset(Cardinality(S), S) = {S}
-
-ASSUME {} \notin kSubset(1, {1,2,3})
-
-ASSUME LET T == 1..3
-       IN \A k \in (1..Cardinality(T)):
-            /\ \A e \in { ss \in (SUBSET T) : Cardinality(ss) = k} :
-                     e \in kSubset(k, T)
-            /\ \A e \in { ss \in (SUBSET T) : Cardinality(ss) # k} :
-                     e \notin kSubset(k, T)
-                     
 ASSUME LET T == {"a","b","c"}
            kSubsetPure(k, S) == { s \in SUBSET S : Cardinality(s) = k }
        IN \A k \in 1..Cardinality(T):