From b65cdc3a1693600cda7a0530a9c94a27732943a5 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Wed, 22 May 2024 18:04:19 +0200 Subject: [PATCH] replace should_widen with wpoint membership checks where appropriate --- src/solver/td3.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index b4f0c28bbe..d916e6df30 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -374,7 +374,7 @@ module Base = if tracing then trace "sol2" "solve still unstable %a" S.Var.pretty_trace x; (solve[@tailcall]) x Widen ) else ( - if term && phase = Widen && should_widen x then ( (* TODO: or use wp? *) + if term && phase = Widen && HM.mem wpoint_gas x then ( (* TODO: or use wp? *) if tracing then trace "sol2" "solve switching to narrow %a" S.Var.pretty_trace x; if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace x; HM.remove stable x; @@ -405,8 +405,7 @@ module Base = HM.replace called y (); let eqd = eq y (eval l x) (side ~x) in HM.remove called y; - (* TODO: is should_widen correct here? *) - if should_widen y then (HM.remove l y; solve y Widen; HM.find rho y) + if HM.mem wpoint_gas y then (HM.remove l y; solve y Widen; HM.find rho y) else (if cache then HM.replace l y eqd; eqd) ) and eval l x y =