As #1413 and the associated regressions show, having more precise (and potentially fewer) contexts is not always beneficial when attempting to prove termination of recursive programs (when we have partial contexts).
It would be interesting to evaluate new constructions here and how helpful they are for the SV-COMP termination categories. Ideas may be:
Baseline: Experiment with full context for all recursive functions in the termination category (disabling the autotuner that disables interval and interval set contexts in recursive calls)
A flavor of context gas (#1340) that starts out with full context and then switches to no-interval in context for recursive procedures
A dedicated construction to always unroll recursion k-deep (via contexts) where k could, e.g., be a function of the magnitude of the argument given to procedures identified as recursive (might capture quite a few SV-COMP style tasks).
...
These are quite disconnected from everything else, and could, e.g., be given to Master's students.
As #1413 and the associated regressions show, having more precise (and potentially fewer) contexts is not always beneficial when attempting to prove termination of recursive programs (when we have partial contexts).
It would be interesting to evaluate new constructions here and how helpful they are for the SV-COMP termination categories. Ideas may be:
These are quite disconnected from everything else, and could, e.g., be given to Master's students.