diff --git a/testcases/verification/Fibonacci.scala b/testcases/verification/Fibonacci.scala
index f2140e54dafb4ff08df3533ae67539db23a67a13..7c37e7ff2a7e39a90a055999c1ec26f97c7a664e 100644
--- a/testcases/verification/Fibonacci.scala
+++ b/testcases/verification/Fibonacci.scala
@@ -1,5 +1,5 @@
 object Fibonacci {
-  def fib(x: Int) : Int = {
+  def fib(x: BigInt) : BigInt = {
     require(x >= 0)
     if(x < 2) {
       x
diff --git a/testcases/verification/Prime.scala b/testcases/verification/Prime.scala
index 11a9f181bba828859c104435433b159aa76e40b8..d8de43f86cf8ec2528e54125dc42148f4cc49e84 100644
--- a/testcases/verification/Prime.scala
+++ b/testcases/verification/Prime.scala
@@ -2,11 +2,11 @@ object Prime {
   // an attempt at defining isPrime in PureScala...
 
   // for positive numbers only
-  def isPrime(i : Int) : Boolean = {
+  def isPrime(i : BigInt) : Boolean = {
     (i >= 2 && noneDivides(2, i))
   }
 
-  def noneDivides(start : Int, number : Int) : Boolean = {
+  def noneDivides(start : BigInt, number : BigInt) : Boolean = {
     if(start == number) {
       true
     } else {
@@ -15,7 +15,7 @@ object Prime {
   }
 
   // for positive numbers only
-  def divides(i : Int, j : Int) : Boolean = {
+  def divides(i : BigInt, j : BigInt) : Boolean = {
     val result = i == j || (i < j && ((j / i) * i == j))
     result
   }
@@ -26,18 +26,18 @@ object Prime {
   } ensuring(res => res)
 
   // Can't seem to get that one to work in reasonable time
-  //  def findTwoLargePrimes(x : Int, y : Int) : Boolean = {
+  //  def findTwoLargePrimes(x : BigInt, y : BigInt) : Boolean = {
   //    x > 200 && y > x && isPrime(x) && isPrime(y)
   //  } ensuring(res => !res)
 
   // Seems to work with lucky tests only :)
-  def findLargePrime(x : Int) : Boolean = {
+  def findLargePrime(x : BigInt) : Boolean = {
     x > 200 && isPrime(x)
   } ensuring(res => !res)
 
   // Just for testing.
   def main(args : Array[String]) : Unit = {
-    def test(n : Int) : Unit = {
+    def test(n : BigInt) : Unit = {
       println("Is " + n + " prime ? -> " + isPrime(n))
     }
     test(119)
diff --git a/testcases/verification/SecondsToTime.scala b/testcases/verification/SecondsToTime.scala
index 6969991c2aa40aa1b6d28c6bc73bf898d2a04fe0..385a72921cce178325579ae098273bcce6cdeabe 100644
--- a/testcases/verification/SecondsToTime.scala
+++ b/testcases/verification/SecondsToTime.scala
@@ -1,20 +1,20 @@
 
 object SecondsToTime {
 
-  def propSum(t: Int, h: Int, m: Int, s: Int) : Boolean = h * 3600 + m * 60 + s == t
-  def prop(t: Int, h: Int, m: Int, s: Int) : Boolean = propSum(t, h, m, s) && m >= 0 && m < 60 && s >= 0 && s < 60 
+  def propSum(t: BigInt, h: BigInt, m: BigInt, s: BigInt) : Boolean = h * 3600 + m * 60 + s == t
+  def prop(t: BigInt, h: BigInt, m: BigInt, s: BigInt) : Boolean = propSum(t, h, m, s) && m >= 0 && m < 60 && s >= 0 && s < 60 
 
-  def secondsToTime(total : Int) = {
+  def secondsToTime(total : BigInt) = {
     require(total >= 0)
       rec(total, total, 0, 0)
   } ensuring(_ match { case (h,m,s) => prop(total, h, m, s) }) 
 
-  def secondsToTime2(total : Int) = {
+  def secondsToTime2(total : BigInt) = {
     require(total >= 0)
       rec2(total, total, 0, 0)
   } ensuring(_ match { case (h,m,s) => prop(total, h, m, s) }) 
 
-  def rec(total : Int, r : Int, h : Int, m : Int) : (Int, Int, Int) = {
+  def rec(total : BigInt, r : BigInt, h : BigInt, m : BigInt) : (BigInt, BigInt, BigInt) = {
     require(propSum(total, h, m, r) && m >= 0 && h >= 0 && r >= 0 && m < 60 && (m == 0 || r + m * 60 < 3600))
 
     if(r >= 3600) {
@@ -26,7 +26,7 @@ object SecondsToTime {
     }
   } ensuring(_ match { case(h,m,s) => prop(total, h, m, s) }) 
 
-  def rec2(total : Int, r : Int, h : Int, m : Int) : (Int, Int, Int) = {
+  def rec2(total : BigInt, r : BigInt, h : BigInt, m : BigInt) : (BigInt, BigInt, BigInt) = {
     require(propSum(total, h, m, r) && m >= 0 && h >= 0 && r >= 0 && m < 60)
     if(r >= 60 && m == 59) {
       rec2(total, r - 60, h + 1, 0)
diff --git a/testcases/verification/TwoSizeFunctions.scala b/testcases/verification/TwoSizeFunctions.scala
index faafa7d181b21054aa794cda74ca6c0188d9a2a3..b5583a70771f363695d144ed16e99315717eccc0 100644
--- a/testcases/verification/TwoSizeFunctions.scala
+++ b/testcases/verification/TwoSizeFunctions.scala
@@ -6,13 +6,13 @@ object TwoSizeFunctions {
   case class Cons(head: Int, tail: List) extends List
   case class Nil() extends List
 
-  def size1(l: List) : Int = (l match {
+  def size1(l: List) : BigInt = (l match {
     case Cons(_, xs) => size1(xs) + 1
     case Nil() => 0
   }) ensuring(_ >= 0)
 
-  def size2(l: List) : Int = size2acc(l, 0)
-  def size2acc(l: List, acc: Int) : Int = {
+  def size2(l: List) : BigInt = size2acc(l, 0)
+  def size2acc(l: List, acc: BigInt) : BigInt = {
     require(acc >= 0)
     l match {
       case Nil() => acc