diff --git a/src/test/resources/regression/synthesis/Examples/Length.scala b/src/test/resources/regression/synthesis/Examples/Length.scala new file mode 100644 index 0000000000000000000000000000000000000000..b8b5aaf89d46c021e38377fbfed9b3de86d0c43d --- /dev/null +++ b/src/test/resources/regression/synthesis/Examples/Length.scala @@ -0,0 +1,14 @@ +import leon.collection._ +import leon.lang._ +import leon.lang.synthesis._ + +object Length { + + def foo(l : List[Int]) : Int = + choose { res:Int => (l, res) passes { + case Nil() => 0 + case Cons(a, Nil()) => 2 + case Cons(_, Cons(_, Cons(_, Cons(_, Nil())))) => 8 + }} + +}