From 14612a56c075611201228ab8bd13476613539ee2 Mon Sep 17 00:00:00 2001 From: Ralf Vogler Date: Thu, 11 Jul 2019 17:41:52 +0200 Subject: [PATCH] cycle detection via side in destabilze does not work for space. 3 tests don't terminate. -> always widen side for space for now. --- src/solvers/td3.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 88f6846b..66f6b122 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -136,7 +136,7 @@ module WP = (* assert (S.Dom.leq old j); assert (S.Dom.leq old w); assert (S.Dom.leq j w); *) - HM.replace rho y ((if HM.mem wpoint y then S.Dom.widen old else identity) (S.Dom.join old d)); + HM.replace rho y ((if HM.mem wpoint y || space then S.Dom.widen old else identity) (S.Dom.join old d)); HM.replace stable y (); if HM.mem wpoint y then destabilize y (* we already are a wpoint, so no need to propagate it anymore *)