More verbosity ; adapt rfollow so that it can be proved

1 files changed, 11 insertions, 1 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 510bf93..6e45240 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -929,6 +929,10 @@ end = struct
             let dc = pass_cycle e d2 in
             let y = edd_join_star_widen e x dc in
 
+            if e.opt.vverbose_ci then
+              Format.printf "d2 %a@. dc %a@. y %a@."
+                edd_print d2 edd_print dc edd_print y;
+
             if e.opt.verbose_ci then
               Format.printf " -> %a@." edd_print y;
 
@@ -945,7 +949,13 @@ end = struct
             let f i =
               let i = edd_meet path i in
               let i' = edd_meet i path_target in
-              let q = edd_join start (pass_cycle e (edd_apply_cl i' e.cl)) in
+              let j = edd_apply_cl i' e.cl in
+
+              if e.opt.vverbose_ci then
+                Format.printf "i %a@.i' %a@.j %a@."
+                  edd_print i edd_print i' edd_print j;
+
+              let q = edd_join start (pass_cycle e j) in
               edd_meet path q
             in