diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 3aa980ef830e44c71455213e3ec914e48018d70e..6015fa8d2cbf5ddefb0d27054e30d38c1c0884b2 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -204,7 +204,7 @@ class CompilationUnit(val ctx: LeonContext,
       gv
 
     case (set : runtime.Set, SetType(b)) =>
-      FiniteSet(set.getElements().asScala.map(jvmToExpr(_, b)).toSeq).setType(SetType(b))
+      FiniteSet(set.getElements().asScala.map(jvmToExpr(_, b)).toSet).setType(SetType(b))
 
     case (map : runtime.Map, MapType(from, to)) =>
       val pairs = map.getElements().asScala.map { entry =>
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 18dbe6ced2b5ca160b69bd61d762a45d8c1d7062..cb3278c096a7f76c96480e85cb151516cad77cb8 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -273,14 +273,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
 
     case SetUnion(s1,s2) =>
       (e(s1), e(s2)) match {
-        case (f@FiniteSet(els1),FiniteSet(els2)) => FiniteSet((els1 ++ els2).distinct).setType(f.getType)
+        case (f@FiniteSet(els1),FiniteSet(els2)) => FiniteSet(els1 ++ els2).setType(f.getType)
         case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
       }
 
     case SetIntersection(s1,s2) =>
       (e(s1), e(s2)) match {
         case (f @ FiniteSet(els1), FiniteSet(els2)) => {
-          val newElems = (els1.toSet intersect els2.toSet).toSeq
+          val newElems = (els1 intersect els2)
           val baseType = f.getType.asInstanceOf[SetType].base
           FiniteSet(newElems).setType(f.getType)
         }
@@ -290,7 +290,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
     case SetDifference(s1,s2) =>
       (e(s1), e(s2)) match {
         case (f @ FiniteSet(els1),FiniteSet(els2)) => {
-          val newElems = (els1.toSet -- els2.toSet).toSeq
+          val newElems = els1 -- els2
           val baseType = f.getType.asInstanceOf[SetType].base
           FiniteSet(newElems).setType(f.getType)
         }
@@ -312,7 +312,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
         case _ => throw EvalError(typeErrorMsg(sr, SetType(Untyped)))
       }
 
-    case f @ FiniteSet(els) => FiniteSet(els.map(e(_)).distinct).setType(f.getType)
+    case f @ FiniteSet(els) => FiniteSet(els.map(e(_))).setType(f.getType)
     case i @ IntLiteral(_) => i
     case b @ BooleanLiteral(_) => b
     case u @ UnitLiteral() => u
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index e2778a3596058fb26906adc6948f33b026ebd1c5..2398e51b979bd38d67b115a123c70d9eee357e2b 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1148,7 +1148,7 @@ trait CodeExtraction extends ASTExtractors {
 
         case ExFiniteSet(tt, args)  =>
           val underlying = extractType(tt)
-          FiniteSet(args.map(extractTree(_))).setType(SetType(underlying))
+          FiniteSet(args.map(extractTree(_)).toSet).setType(SetType(underlying))
 
         case ExFiniteMultiset(tt, args) =>
           val underlying = extractType(tt)
@@ -1156,7 +1156,7 @@ trait CodeExtraction extends ASTExtractors {
 
         case ExEmptySet(tt) =>
           val underlying = extractType(tt)
-          FiniteSet(Seq()).setType(SetType(underlying))
+          FiniteSet(Set()).setType(SetType(underlying))
 
         case ExEmptyMultiset(tt) =>
           val underlying = extractType(tt)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 11a2e7281ed2cbb233233a2a6e2d1db0dd597a06..be2a14fa5f6a44a84f53cfa63705438babfc0a7f 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -93,12 +93,12 @@ object Extractors {
       case And(args) => Some((args, And.apply))
       case Or(args) => Some((args, Or.apply))
       case FiniteSet(args) =>
-        Some((args,
+        Some((args.toSeq,
               { newargs =>
                 if (newargs.isEmpty) {
-                  FiniteSet(Seq()).setType(expr.getType)
+                  FiniteSet(Set()).setType(expr.getType)
                 } else {
-                  FiniteSet(newargs)
+                  FiniteSet(newargs.toSet)
                 }
               }
             ))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 5d97ff9891c62b61f8fc0827b5f25036fc7f14b7..aafaff7539ee0f63550687f081ce55a386defc92 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -262,7 +262,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
       case GreaterThan(l,r)          => optP { p"$l > $r" }
       case LessEquals(l,r)           => optP { p"$l <= $r" }
       case GreaterEquals(l,r)        => optP { p"$l >= $r" }
-      case FiniteSet(rs)             => p"{$rs}"
+      case FiniteSet(rs)             => p"{${rs.toSeq}}"
       case FiniteMultiset(rs)        => p"{|$rs|)"
       case EmptyMultiset(_)          => p"\u2205"
       case Not(ElementOfSet(e,s))    => p"$e \u2209 $s"
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 8305781b9834418331d446681ab2eb621d037071..f51674901d7862bf49a137640ed9230b1bf81c29 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -26,7 +26,8 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
       case Iff(l,r)             => p"$l == $r"
       case Implies(l,r)         => pp(Or(Not(l), r))
       case Choose(vars, pred)   => p"choose((${typed(vars)}) => $pred)"
-      case s @ FiniteSet(rs)    => {
+      case s @ FiniteSet(rss)    => {
+        val rs = rss.toSeq
         s.getType match {
           case SetType(ut) =>
             p"Set[$ut]($rs)"
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index e9e2c66b15c05b29d796fb9a529cc74c5ec6c9fb..67cec4c0e39105361c8fa84358a1c012f1a44a97 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -780,7 +780,7 @@ object TreeOps {
   def simplestValue(tpe: TypeTree) : Expr = tpe match {
     case Int32Type                  => IntLiteral(0)
     case BooleanType                => BooleanLiteral(false)
-    case SetType(baseType)          => FiniteSet(Seq()).setType(tpe)
+    case SetType(baseType)          => FiniteSet(Set()).setType(tpe)
     case MapType(fromType, toType)  => FiniteMap(Seq()).setType(tpe)
     case TupleType(tpes)            => Tuple(tpes.map(simplestValue))
     case ArrayType(tpe)             => ArrayFill(IntLiteral(0), simplestValue(tpe))
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 7f5d5f4c64966890842fb5c57699e34c7dff358f..44b98012a2ef65bf0b5dd570daab9750d4de265f 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -519,8 +519,8 @@ object Trees {
   }
 
   /* Set expressions */
-  case class FiniteSet(elements: Seq[Expr]) extends Expr {
-    val tpe = if (elements.isEmpty) None else leastUpperBound(elements.map(_.getType))
+  case class FiniteSet(elements: Set[Expr]) extends Expr {
+    val tpe = if (elements.isEmpty) None else leastUpperBound(elements.toSeq.map(_.getType))
     tpe.foreach(t => setType(SetType(t)))
   }
   // TODO : Figure out what evaluation order is, for this.
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index 0cb7e3c6eb79588a43c5978dcc48ec80c1721dc8..469b7606b6fdb9756c092e29f740164ab716582d 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -255,7 +255,7 @@ object TypeTreeOps {
             Error(desc).setType(tpeSub(e.getType)).copiedFrom(e)
 
           case s @ FiniteSet(elements) if elements.isEmpty =>
-            FiniteSet(Nil).setType(tpeSub(s.getType)).copiedFrom(s)
+            FiniteSet(Set()).setType(tpeSub(s.getType)).copiedFrom(s)
 
           case v @ Variable(id) if idsMap contains id =>
             Variable(idsMap(id)).copiedFrom(v)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index d26e4d47d39c4036c5c6e060c005143ef4323853..92907a2e7e364ec3cde844aae839c260c79a28b3 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -45,15 +45,15 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
       GenericValue(tp, n.toInt)
 
     case (QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset"), Seq()), _), SetType(base)) =>
-      FiniteSet(Seq()).setType(tpe)
+      FiniteSet(Set()).setType(tpe)
 
     case (FunctionApplication(SimpleSymbol(SSymbol("setenum")), elems), SetType(base)) =>
-      FiniteSet(elems.map(fromSMT(_, base))).setType(tpe)
+      FiniteSet(elems.map(fromSMT(_, base)).toSet).setType(tpe)
 
     case (FunctionApplication(SimpleSymbol(SSymbol("union")), elems), SetType(base)) =>
       FiniteSet(elems.map(fromSMT(_, tpe) match {
         case FiniteSet(elems) => elems
-      }).flatten).setType(tpe)
+      }).flatten.toSet).setType(tpe)
 
     case _ =>
       super[SMTLIBTarget].fromSMT(s, tpe)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 4feb6a3942ae8b61351eb255301538f97b59762e..48d602402818ae0b403ba3d34f722f4e9b17eec6 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -234,7 +234,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
     case SetType(base) =>
       assert(r.default == BooleanLiteral(false) && r.keyTpe == base)
 
-      FiniteSet(r.elems.keySet.toSeq).setType(tpe)
+      FiniteSet(r.elems.keySet).setType(tpe)
 
     case RawArrayType(from, to) =>
       r
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 077602062d66da678af1d8294efb38180f36e89c..1529dc7f7d7b0c4ad14c87fb7ac41d284aa3a7a5 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -749,7 +749,7 @@ trait AbstractZ3Solver
                   case None => throw new CantTranslateException(t)
                   case Some(set) =>
                     val elems = set.map(e => rec(e))
-                    FiniteSet(elems.toSeq).setType(tpe)
+                    FiniteSet(elems).setType(tpe)
                 }
 
               case LeonType(UnitType) =>
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
index f17f75c960319464ba0fac0eae2e7f5a9ac65661..faaa084e57a6f62f1efa68d45a84e12784eccb0a 100644
--- a/src/main/scala/leon/synthesis/rules/Tegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -71,7 +71,7 @@ case object TEGIS extends Rule("TEGIS") {
 
             case st @ SetType(base) =>
               List(
-                Generator(List(base),   { case elems     => FiniteSet(elems).setType(st) }),
+                Generator(List(base),   { case elems     => FiniteSet(elems.toSet).setType(st) }),
                 Generator(List(st, st), { case Seq(a, b) => SetUnion(a, b) }),
                 Generator(List(st, st), { case Seq(a, b) => SetIntersection(a, b) }),
                 Generator(List(st, st), { case Seq(a, b) => SetDifference(a, b) })
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 84c546c05ae00b67e347fff264ce9a249fd18bf8..678373a8968f5aa079ed1dc1964c8a1bd23edc56 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -315,9 +315,9 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
     val nil = mkCaseClass("Nil")
     val cons12 = mkCaseClass("Cons", IL(1), mkCaseClass("Cons", IL(2), mkCaseClass("Nil")))
 
-    val semp = FiniteSet(Seq.empty).setType(SetType(Int32Type))
-    val s123 = FiniteSet(Seq(IL(1), IL(2), IL(3))).setType(SetType(Int32Type))
-    val s246 = FiniteSet(Seq(IL(2), IL(4), IL(6))).setType(SetType(Int32Type))
+    val semp = FiniteSet(Set()).setType(SetType(Int32Type))
+    val s123 = FiniteSet(Set(IL(1), IL(2), IL(3))).setType(SetType(Int32Type))
+    val s246 = FiniteSet(Set(IL(2), IL(4), IL(6))).setType(SetType(Int32Type))
 
     for(e <- evaluators) {
       checkSetComp(e, mkCall("finite"), Set(1, 2, 3))