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

1 files changed, 17 insertions, 13 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;