diff --git a/testcases/synthesis/DrSuter.scala b/testcases/synthesis/DrSuter.scala new file mode 100644 index 0000000000000000000000000000000000000000..0ce54f5b575fe3a1a3b987f903d11aeba01e00c4 --- /dev/null +++ b/testcases/synthesis/DrSuter.scala @@ -0,0 +1,17 @@ +import leon.Utils._ + +object DrSuter { + + abstract class List + case class Nil() extends List + case class Cons(head : Int, tail : List) extends List + + + + def myChoose(a : List) : (Int,Int,List) = { + choose { (x: Int, y: Int, ys: List) => + Cons(x, Cons(y, ys)) == a && x == y || + Cons(x, ys) == a && x < 0 + } + } +}