diff --git a/testcases/testgen/List.scala b/testcases/testgen/List.scala new file mode 100644 index 0000000000000000000000000000000000000000..8d436d370ddbfecd00dcd67a085dc5230e55905f --- /dev/null +++ b/testcases/testgen/List.scala @@ -0,0 +1,14 @@ +import leon.Utils._ + +object List { + + abstract class 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) + case Nil() => 0 + })) ensuring(_ >= 0) + +}