diff --git a/testcases/Choose.scala b/testcases/Choose.scala
index 09f606b2115dcf8aec6c4f1e29c257f891f98f44..85b6225d727b8016b3fc9e2c30dc4c98c59b46f2 100644
--- a/testcases/Choose.scala
+++ b/testcases/Choose.scala
@@ -13,4 +13,17 @@ object ChooseTest {
   def c4(a: Int): (Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int) => x1 > a && x2 > a }
   def c5(a: Int): (Int, Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int, x5: Int) => x1 > a && x2 > a }
 
+
+  sealed abstract class List
+  case class Nil() extends List
+  case class Cons(head : Int, tail : List) extends List
+
+  def size(lst : List) : Int = (lst match {
+    case Nil() => 0
+    case Cons(_, xs) => 1 + size(xs)
+  }) ensuring(_ >= 0)
+
+  def k0() : List = choose {
+    (l : List) => size(l) == 1
+  }
 }