Invalid conterexample in ScanLeft

[fengwz17]

I wonder how to provide pre- conditions for expression like ScanLeft.

Given the following code,

val a = BigInt(0)
val list = List(BigInt(0), BigInt(1), BigInt(2))
assert(list.forall(_ >= BigInt(0)))
val lll = list.scanLeft(a) { case (y, j) =>
    assert(j >= 0)
    y + j
} 
assert(lll.last == BigInt(3))

The assertion assert(j >= 0) is reported invalid with a counterexample

[ Debug  ]  - Now solving 'body assertion' VC for foo @32:14...
[ Debug  ] BigInt("0") > x || x > BigInt("5") || !forall[BigInt](Cons[BigInt](BigInt("0"), Cons[BigInt](BigInt("1"), Cons[BigInt](BigInt("2"), Nil[BigInt]()))), (_$1: BigInt) => _$1 >= BigInt("0")) || x$2 >= BigInt("0")
[ Debug  ] Solving with: U:smt-z3
[Warning ]  - Result for 'body assertion' VC for foo @32:14:
[Warning ] stain/src/main/scala/verify/try/whileExample.scala:32:14:  => INVALID
                 assert(j >= 0)
                        ^^^^^^
[Warning ] Found counter-example:
[Warning ]   x$2: BigInt -> BigInt("-1")
[Warning ]   x: BigInt   -> BigInt("0")

Seems that it is beacause the information of list is not provided to ScanLeft, so how to provide such property in ScanLeft? (It cannot be provided by require as a function call)

[mario-bucev]

Hello! This "works as expected" because VCs generation within lambdas is modular: that is the inputs passed to the lambdas is not constrained (see comment https://github.com/epfl-lara/stainless/issues/1370#issuecomment-1359865635).

[fengwz17]

Hello! This "works as expected" because VCs generation within lambdas is modular: that is the inputs passed to the lambdas is not constrained (see comment #1370 (comment)).

I see, thanks!