diff --git a/library/lang/Set.scala b/library/lang/Set.scala
index 36c70a8372dd7a81d1737dfd321e81839d38fe6f..8f4595d33fada35acfa38435c3cd542116cf3cbd 100644
--- a/library/lang/Set.scala
+++ b/library/lang/Set.scala
@@ -17,6 +17,7 @@ case class Set[T](val theSet: scala.collection.immutable.Set[T]) {
    def ++(a: Set[T]): Set[T] = new Set[T](theSet ++ a.theSet)
    def -(a: T): Set[T] = new Set[T](theSet - a)
    def --(a: Set[T]): Set[T] = new Set[T](theSet -- a.theSet)
+   def size: BigInt = theSet.size
    def contains(a: T): Boolean = theSet.contains(a)
    def isEmpty: Boolean = theSet.isEmpty
    def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)
diff --git a/src/main/java/leon/codegen/runtime/Set.java b/src/main/java/leon/codegen/runtime/Set.java
index 965aa20df6ba453e2fcbdfb0c2e4afce66d29d27..522dbe6589eac54bf2acac3e1f81ee4b4c7c962c 100644
--- a/src/main/java/leon/codegen/runtime/Set.java
+++ b/src/main/java/leon/codegen/runtime/Set.java
@@ -49,8 +49,8 @@ public final class Set {
     return true;
   }
 
-  public int size() {
-    return _underlying.size();
+  public BigInt size() {
+    return new BigInt(""+_underlying.size());
   }
 
   public Set union(Set s) {
@@ -84,7 +84,7 @@ public final class Set {
 
     Set other = (Set)that;
 
-    return this.size() == other.size() && this.subsetOf(other);
+    return this.size().equals(other.size()) && this.subsetOf(other);
   }
 
   @Override
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 6543da029ecfc52bf4297531d6be30b048b3a5c3..85ed5eb0be33daa2797d08a004048ebf2da8ac17 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -654,7 +654,7 @@ trait CodeGeneration {
 
       case SetCardinality(s) =>
         mkExpr(s, ch)
-        ch << InvokeVirtual(SetClass, "size", "()I")
+        ch << InvokeVirtual(SetClass, "size", s"()$BigIntClass;")
 
       case SubsetOf(s1, s2) =>
         mkExpr(s1, ch)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 216f51c5d8aba35c38fd72723d35f3dcf460e44b..fccda2aeabd69b72bef9690e8f55fa61a562911c 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -504,7 +504,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
     case SetCardinality(s) =>
       val sr = e(s)
       sr match {
-        case FiniteSet(els, _) => IntLiteral(els.size)
+        case FiniteSet(els, _) => InfiniteIntegerLiteral(els.size)
         case _ => throw EvalError(typeErrorMsg(sr, SetType(Untyped)))
       }
 
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 0a75dfebc5ae78d8147d0f601d61d38e2e0c05e2..77a6c719f8f4d0c06766982456b6a094545512ce 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1623,6 +1623,9 @@ trait CodeExtraction extends ASTExtractors {
               or(a1, a2)
 
             // Set methods
+            case (IsTyped(a1, SetType(b1)), "size", Nil) =>
+              SetCardinality(a1)
+
             //case (IsTyped(a1, SetType(b1)), "min", Nil) =>
             //  SetMin(a1)
 
@@ -1842,7 +1845,11 @@ trait CodeExtraction extends ASTExtractors {
       case AnnotatedType(_, tpe) => extractType(tpe)
 
       case _ =>
-        outOfSubsetError(tpt.typeSymbol.pos, "Could not extract type as PureScala: "+tpt+" ("+tpt.getClass+")")
+        if (tpt ne null) {
+          outOfSubsetError(tpt.typeSymbol.pos, "Could not extract type as PureScala: "+tpt+" ("+tpt.getClass+")")
+        } else {
+          outOfSubsetError(NoPosition, "Tree with null-pointer as type found")
+        }
     }
 
     private def getClassType(sym: Symbol, tps: List[LeonType])(implicit dctx: DefContext) = {
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index b834eb9f1270bca728b2cdbaa63bb98a37b0dd49..6e9adae5f6ee3548b1fa70af41b127e6a46a76b4 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -765,7 +765,7 @@ object Expressions {
   }
   /** $encodingof `set.length` */
   case class SetCardinality(set: Expr) extends Expr {
-    val getType = Int32Type
+    val getType = IntegerType
   }
   /** $encodingof `set.subsetOf(set2)` */
   case class SubsetOf(set1: Expr, set2: Expr) extends Expr {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index cb1c3246d7eff487e00904c3acbd61d7068aa316..3173dd652e06e1cc771589490ff6b4825a284231 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -138,6 +138,9 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
     case ElementOfSet(e, s) =>
       FunctionApplication(SSymbol("member"), Seq(toSMT(e), toSMT(s)))
 
+    case SetCardinality(s) =>
+      FunctionApplication(SSymbol("card"), Seq(toSMT(s)))
+
     case SetDifference(a, b) =>
       FunctionApplication(SSymbol("setminus"), Seq(toSMT(a), toSMT(b)))