diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 8837ee937c89adb0593d5a2ec0e208162dbcb2e3..5c2571719c4a54f18c2252e1aca596862ff8139f 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -88,7 +88,17 @@ object Extractors {
       case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
       case And(args) => Some((args, And.apply))
       case Or(args) => Some((args, Or.apply))
-      case FiniteSet(args) => Some((args, FiniteSet))
+      case FiniteSet(args) =>
+        Some((args,
+              { newargs =>
+                if (newargs.isEmpty) {
+                  FiniteSet(Seq()).setType(expr.getType)
+                } else {
+                  FiniteSet(newargs)
+                }
+              }
+            ))
+
       case FiniteMap(args) => {
         val subArgs = args.flatMap{case (k, v) => Seq(k, v)}
         val builder: (Seq[Expr]) => Expr = (as: Seq[Expr]) => {