diff --git a/src/solver/td3.ml b/src/solver/td3.ml
index 7e2a18b042..c7bec621e3 100644
--- a/src/solver/td3.ml
+++ b/src/solver/td3.ml
@@ -284,7 +284,11 @@ module Base =
             let was_stable = HM.mem stable y in
             HM.remove stable y;
             HM.remove superstable y;
-            HM.mem called y || destabilize_vs y || b || was_stable && List.mem_cmp S.Var.compare y vs
+            Hooks.stable_remove y;
+            if not (HM.mem called y) then
+              destabilize_vs y || b || was_stable && List.mem_cmp S.Var.compare y vs
+            else
+              true
           ) w false
       and solve ?reuse_eq x phase =
         if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x);