I think the reason we kept it so far is because there's a distinct check there

HM.mem called y || destabilize_vs y || b || was_stable && List.mem_cmp S.Var.compare y vs

The key question would be why that check is different and why that is.

As I understand, the check is different because the side_widen: "cycle" strategy wants to know, whether the function destabilized any stable start variables or called variables.

HM.mem called y || destabilize_vs y

is effectively equivalent to

if not (HM.mem called y) then destabilize_vs y else true

So it behaves the same, except that it also returns this boolean. As mentioned in #1434, this boolean whether a start var etc. was destabilized could be computed in an optional callback action (including the remainder of the check || b || was_stable && List.mem_cmp S.Var.compare y vs)

I had another look, and not calling the Hook seems like it was clearly an oversight.

Not using destab_with_sides on the other hand seems odd at a first glance. However, it seems like destabilize_ref is only setting to destab_with_sides during restarting and destablize_vs is only used from side which only happens during the actual solve

destabilize_ref := destabilize_normal; (* always use normal destabilize during actual solve *)

Maybe it suffices to add the call to the Hook, add these observations as a remark and remove the usage of || got control flow as a more conservative solution than #1434.

What do you think @Red-Panda64 @sim642?

Adding the hook call isn't controversial I think. I don't understand what's the issue with || though, they both recurse if not in called.

It's a clean code thing, I find the more explicit

if not (HM.mem called y) then destabilize_vs y else true

to be a lot more readable than the formulation with ||. I'd be surprised if there's any performance differences between both styles.

But it's also not a hill I'm willing to die on 😉

I stand by the opinion that the duplicate code itself is problematic. Namely, that adjustments of either destabilize or destabilize_vs could accidentally not be applied to the other. This does happen, the missing Hook call proves this.

Of course, if you think think the cost of refactoring this outweighs the benefits, we can also just add the Hook and call it a day. As for the short-circuiting ||, I don't see a reason not to make this more explicit, if we are already making small adjustments to destabilize_vs. I think that short-circuiting with side-effects leads to a bit more confusing code whereas removing it should be uncontroversial.

It's a clean code thing, I find the more explicit

if not (HM.mem called y) then destabilize_vs y else true

to be a lot more readable than the formulation with ||. I'd be surprised if there's any performance differences between both styles.

Ah, that seems reasonable.

I thought there might've been some subtle issue with the recursion not happening in some cases when it should've. For example, reordering the disjuncts could easily cause this (e.g. putting b before the recursive call). They are in the correct order right now, but an explicit if (with a comment indicating the intent) would avoid such issue being introduced in the future.

As to the code duplication, destabilize_with_side is an even worse offender with very similar loops (only over different sets):