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

2 files changed, 38 insertions, 25 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 0db128f..c3db657 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -412,19 +412,23 @@ end = struct
 
         let i = dd_singleton st.d_vars z in
         let j = cycle st st.cl i in
-        let cases = ref [] in
-        Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data;
-        List.iter
-            (fun case ->
-              let i' = set_target_case st i case in
-              let j = cycle st st.cl i' in
-              Hashtbl.iter (fun _ q -> add_case st q) j.data)
-            !cases;
-
-        st.delta <- List.filter ((<>) case) st.delta;
-
-        if st.opt.verbose_ci then
-          Format.printf "-> @[<hov>%a@]@." print_st st;
+        if Hashtbl.length j.data = 0 then
+          Format.printf "@.WARNING: contradictory hypotheses!@.@."
+        else begin
+          let cases = ref [] in
+          Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data;
+          List.iter
+              (fun case ->
+                let i' = set_target_case st i case in
+                let j = cycle st st.cl i' in
+                Hashtbl.iter (fun _ q -> add_case st q) j.data)
+              !cases;
+
+          st.delta <- List.filter ((<>) case) st.delta;
+
+          if st.opt.verbose_ci then
+            Format.printf "-> @[<hov>%a@]@." print_st st;
+        end
 
       done;
 
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