Closed vkuncak closed 9 months ago
Trying to verify this:
import stainless.lang.* import stainless.collection.* import stainless.annotation.* def foldListConc[T,S](l1: List[T], l2: List[T], s0: S, seqop: (S,T) => S): Unit = { l1 match case Nil() => () case Cons(t1,l1rest) => { assert(l1 ++ l2 == Cons(t1, l1rest ++ l2), "head of concat") assert((l1 ++ l2).foldLeft(s0)(seqop) == (l1rest ++ l2).foldLeft(seqop(s0, t1))(seqop)) foldListConc(l1rest, l2, s0, seqop) } } ensuring(_ => (l1 ++ l2).foldLeft(s0)(seqop) == l2.foldLeft(l1.foldLeft(s0)(seqop))(seqop))
gives the error that misleading suggests that an assert has failed, which is not the case, rather the postcondition fails:
warning: - Result for 'postcondition' VC for foldListConc @11:7: warning: l1.isInstanceOf[Nil] || ++[T](l1, l2) != Cons[T](l1.h, ++[T](l1.t, l2)) || foldLeft[T, S](++[T](l1, l2), s0, seqop) != foldLeft[T, S](++[T](l1.t, l2), seqop(s0, l1.h), seqop) || { val _$1: Unit = foldListConc[T, S](l1.t, l2, s0, seqop) foldLeft[T, S](++[T](l1, l2), s0, seqop) == foldLeft[T, S](l2, foldLeft[T, S](l1, s0, seqop), seqop) } PositionsError.scala:11:7: warning: => TIMEOUT assert(l1 ++ l2 == Cons(t1, l1rest ++ l2), "head of concat") ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Trying to verify this:
gives the error that misleading suggests that an assert has failed, which is not the case, rather the postcondition fails: