diff options
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 28 |
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; |