diff options
| -rw-r--r-- | abstract/abs_interp.ml | 30 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 33 |
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 |