Add message when a step goes on BOT, ie. contradiction in assumes.

1 files changed, 21 insertions, 12 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index cdcdab2..1eac551 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -946,17 +946,21 @@ end = struct
 
             let d2 = edd_apply_cl x e.cl in
             let dc = pass_cycle e d2 in
-            let y = edd_star_new x (edd_accumulate e x dc) in
+            if dc.root = DBot then begin
+              Format.printf "@.WARNING: contradictory hypotheses!@.@.";
+              x
+            end else begin
+              let y = edd_star_new x (edd_accumulate 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;
+              if e.opt.vverbose_ci then
+                Format.printf "d2 %a@. dc %a@. y %a@."
+                  edd_print d2 edd_print dc edd_print y;
 
-            if not (edd_eq x y) then ch_it (n+1) y else y
+              if e.opt.verbose_ci then
+                Format.printf " -> %a@." edd_print y;
 
+              if not (edd_eq x y) then ch_it (n+1) y else y
+            end
           | Some i ->
             let path = edd_extract_path x i in
             let x = edd_unstar x i in
@@ -993,12 +997,17 @@ end = struct
 
 
             let fj = pass_cycle e (edd_apply_cl z e.cl) in
-            let r = edd_star_new x (edd_accumulate e x fj) in
+            if fj.root = DBot then begin
+              Format.printf "@.WARNING: contradictory hypotheses!@.@.";
+              x
+            end else begin
+              let r = edd_star_new x (edd_accumulate e x fj) in
 
-            if e.opt.verbose_ci then
-              Format.printf " -> %a@." edd_print r;
+              if e.opt.verbose_ci then
+                Format.printf " -> %a@." edd_print r;
 
-            ch_it (n+1) r
+              ch_it (n+1) r
+            end
         in
 
         let init_acc = edd_star_new (edd_bot e.data.ve) e.data in