From 0ce4cf6e7e280269db5da7c7b4fcb977b7f6f2cd Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 4 Jul 2014 17:49:57 +0200 Subject: Warning for contradictory hypotheses was wrong. --- abstract/abs_interp.ml | 28 +++++++++++++--------------- 1 file 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 "-> @[%a@]@." print_st st; - if st.opt.verbose_ci then - Format.printf "-> @[%a@]@." print_st st; - end + st.delta <- List.filter ((<>) case) st.delta; done; -- cgit v1.2.3