cycle detection via side in destabilze does not work for space. 3 tes…

…ts don't terminate. -> always widen side for space for now.
jerhard · Jul 12, 2019 · 14612a5 · 14612a5
1 parent 217ba0d
commit 14612a5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 *)