leon
leon copied to clipboard
Evaluation of passes fails to record positions of patterns, guards, scrutinees
The counter-example is not well displayed within the passes:
package leon.custom
import leon._
import leon.lang._
import leon.collection._
import leon.annotation._
sealed abstract class List[T] {
def count(e: T): BigInt = { this match {
case Cons(h, t) =>
if (h == e) {
t.count(e)
} else {
t.count(e)
}
case Nil() =>
BigInt(0)
}} ensuring { res =>
(((this, e), res) passes {
case (Cons(a1, Cons(a2, Cons(a3, Cons(a4, Nil())))), v) if a1 == v && a2 == v && a3 != v && a4 == v => 3
case (Cons(a1, Cons(a2, Nil())), v) if a1 != v && a2 != v => 0
})
}
}
case class Cons[T](h: T, t: List[T]) extends List[T]
case class Nil[T]() extends List[T]
What is it supposed to display ? Or where ?