update List

testcases/testgen/List.scala

 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
+  }
 }