The timeouts are related to __VERIFIER_assert also being identified as an abortUnless function. Apron analysis refining according to that somehow breaks things.

The recursified_knuth timeout is acceptable. It is caused by new refinement from assume_abort_if_not(a > 0); which somehow causes an explosion of contexts. This happens even with just def_exc, no intervals or anything of infinite height is needed. Tracing shows contexts increasing like Not {160}, ..., Not {240}, etc. So one exclusion in the context leads to a different exclusion in the recursive call.

This is a more fundamental problem that's not caused by abortUnless. Context widening fixes the timeout, but our svcomp conf doesn't use it (probably for more precision on recursive tasks that finish in time).

Context widening fixes the timeout, but our svcomp conf doesn't use it (probably for more precision on recursive tasks that finish in time).

This might the sort of thing where the context gas ⛽ may pay off.

What's the holdup here? If no one else wants to review it, I'd suggest we merge it.

The holdup is that this depends on #1462 to prevent everything from just crashing. And that in itself depends on #1470 being in place first to avoid other regressions.