diff --git a/testcases/testgen/List.scala b/testcases/testgen/List.scala
index 8d436d370ddbfecd00dcd67a085dc5230e55905f..b21928d924998d5dcd89ea2c278928c77aecf46a 100644
--- a/testcases/testgen/List.scala
+++ b/testcases/testgen/List.scala
@@ -1,4 +1,5 @@
 import leon.Utils._
+import leon.Annotations._
 
 object List {
 
@@ -6,9 +7,14 @@ object List {
   case class Cons(head: Int, tail: List) extends List
   case class Nil() extends List
 
-  def size(l: List): Int = waypoint(1, (l match {
-    case Cons(_, tail) => 1 + size(tail)
+  @main
+  def size(l: List): Int = (l match {
+    case Cons(_, tail) => sizeTail(tail, 1)
     case Nil() => 0
-  })) ensuring(_ >= 0)
+  }) ensuring(_ >= 0)
 
+  def sizeTail(l2: List, acc: Int): Int = l2 match {
+    case Cons(_, tail) => sizeTail(tail, acc+1)
+    case Nil() => acc
+  }
 }