diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index dfd099bcc592688fd24dbeff2bc6ed930df42cbc..edd9e7dc87fd89f81640187204611266de513813 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -220,9 +220,9 @@ trait ASTExtractors {
     }
 
     object ExBigIntLiteral {
-      def unapply(tree: Tree): Option[Int] = tree  match {
-        case Apply(ExSelected("scala", "package", "BigInt", "apply"), (n: Literal) :: Nil) =>
-          Some(n.value.intValue)
+      def unapply(tree: Tree): Option[Tree] = tree  match {
+        case Apply(ExSelected("scala", "package", "BigInt", "apply"), n :: Nil) =>
+          Some(n)
         case _ =>
           None
       }
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 7acbe71754349e47896a840d5260cd234845bb7a..13aefc5b756b3e72cc745fbccaa20d34937cf579 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1204,9 +1204,10 @@ trait CodeExtraction extends ASTExtractors {
           val newValueRec = extractTree(newValue)
           ArrayUpdate(lhsRec, indexRec, newValueRec)
 
-        case ExBigIntLiteral(n) => {
-          InfiniteIntegerLiteral(BigInt(n))
+        case ExBigIntLiteral(n: Literal) => {
+          InfiniteIntegerLiteral(BigInt(n.value.stringValue))
         }
+        case ExBigIntLiteral(n) => outOfSubsetError(tr, "Non-literal BigInt constructor")
 
         case ExIntToBigInt(tree) => {
           val rec = extractTree(tree)
@@ -1214,7 +1215,7 @@ trait CodeExtraction extends ASTExtractors {
             case IntLiteral(n) =>
               InfiniteIntegerLiteral(BigInt(n))
             case _ => 
-              IntToBigInt(rec)
+              outOfSubsetError(tr, "Conversion from Int to BigInt")
           }
         }
 
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 60b6eb3fb9f1e69ac8e4152ffc374a6390b31a63..278d66f665fb8da0883994aa9ed6638c2c6b5ad5 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -394,10 +394,6 @@ object Trees {
     val getType = Int32Type
   }
 
-  case class IntToBigInt(expr: Expr) extends Expr {
-    val getType = Int32Type
-  }
-
   /* Set expressions */
   case class FiniteSet(elements: Set[Expr]) extends Expr with MutableTyped {
     val tpe = if (elements.isEmpty) None else leastUpperBound(elements.toSeq.map(_.getType))
diff --git a/src/test/resources/regression/verification/purescala/error/ConvertBigInt.scala b/src/test/resources/regression/verification/purescala/error/ConvertBigInt.scala
new file mode 100644
index 0000000000000000000000000000000000000000..41e209a10bec9bd05ea05016b439f14b7a38fd1f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/error/ConvertBigInt.scala
@@ -0,0 +1,7 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object ConvertBigInt {
+
+  def safeInt(x: Int): BigInt = x
+
+}
diff --git a/src/test/resources/regression/verification/purescala/error/LiteralBigInt.scala b/src/test/resources/regression/verification/purescala/error/LiteralBigInt.scala
new file mode 100644
index 0000000000000000000000000000000000000000..67783edc84531b9081942e3e453499cfbb3e5441
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/error/LiteralBigInt.scala
@@ -0,0 +1,7 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object LiteralBigInt {
+
+  def safeInt(x: Int): BigInt = BigInt(x)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/FoolProofAdder.scala b/src/test/resources/regression/verification/purescala/valid/FoolProofAdder.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4fd46f85fc051b8de8d1025e74a7a6a6275e0611
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/FoolProofAdder.scala
@@ -0,0 +1,11 @@
+import leon.annotation._
+import leon.lang._
+
+object FoolProofAdder {
+
+  def foolProofAdder(x: BigInt): BigInt = {
+    require(x > 0)
+    x + BigInt(999999) + BigInt("999999999999999")
+  } ensuring(_ > 0)
+
+}