Closed samuelchassot closed 1 month ago
I'm working on the test suite.
Example of function that does not work for now:
def hoRecur(x: BigInt, f: BigInt => BigInt): BigInt = {
require(x >= 0 && forall((x: BigInt) => f(x) < x && f(x) >= 0))
decreases(x)
if (x <= 0) BigInt(0)
else
hoRecur(f(x), f)
}
The issue is in the UnrollingSolver
, when the model is evaluated in the axioms in the templates.
I'm exploring other ways to construct the VC that would avoid this.
The crash happens as well with the function hoRecur
if we add a wrong post condition like .ensuring(res => res > 1)
. I don't know yet if it is a bug, or an expected behaviour of Stainless when dealing with quantifiers.
It is also slower to prove those VCs than I expected: with a timeout of 180s on the LongMap verification, 16/171 time out. Given this fact, I will make it optional for now.
Add a SAT check for preconditions. Example of usage:
outputs: