We have quite often suspected excessive widening at unknowns that receive side-effects (e.g. function entry nodes) as a cause of unnecessary precision-loss.

In a brainstorming session with @stilscher and @hseidl we came up with a possible solution. Instead of making an unknown a point after having received 2 increasing side-effects, one could generalize this to allow n increasing side-effects before making the unknown a widening point.

This should be able to do in an extensible way by replacing the point data structure by a customizable module that receives the information whether a side-effects increased the abstract value and is queried instead of point.
This might also cleanup many of the existing options we already have concerning handling widening of side-effects.

The same logic could in principle also apply to other unknowns, which would mostly concern loop heads by delaying widening. This seems like one would get it for free after implementing the idea above.

(The title of the issue is a pun on gas 💨, maybe ⛽ would be the more serious emoji, provided emoji can be serious)

The question then is whether @stilscher wants to do this herself or whether we should give it to a Master's student. Another alternative would be giving it to Ali if he wants to start contributing to the solver as a project to catch a foothold before moving on to the 🧵-TD3 (#644).