Warning for contradictory hypotheses was wrong.

1 files changed, 13 insertions, 15 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index c3db657..f6ce0ab 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -412,23 +412,21 @@ end = struct
 
         let i = dd_singleton st.d_vars z in
         let j = cycle st st.cl i in
-        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;
+        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;
+
+
+        if st.opt.verbose_ci then
+          Format.printf "-> @[<hov>%a@]@." print_st st;
 
-          if st.opt.verbose_ci then
-            Format.printf "-> @[<hov>%a@]@." print_st st;
-        end
+        st.delta <- List.filter ((<>) case) st.delta;
 
       done;