From 1082f1c2afeb10ab5f8ddd8fb77a63b3e64b4bc6 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Mon, 3 Jun 2024 08:48:25 +0200 Subject: [PATCH] add missing stable_remove hook to destabilize_vs --- src/solver/td3.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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);