search

epfl-lara / inox

Solver for higher-order functional programs, used by Stainless
Apache License 2.0
88 stars 20 forks source link

Provision timeout in unrolling solver #223

Open samuelchassot opened 1 week ago

samuelchassot commented 1 week ago

Idea: provision the timeout for more than 1 unrolling to avoid spending the entire timeout in the first unrolling step. This would (maybe) allow the automatic verification of properties that are true under K-induction, as it would try to unroll even if the solver does not return anything.

vkuncak commented 1 week ago

@sankalpgambhir this might interest you as well