summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 17:49:57 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-04 17:49:57 +0200
commit0ce4cf6e7e280269db5da7c7b4fcb977b7f6f2cd (patch)
treeea0e8087bc87728f517f4367f4a50656d950bf5b
parent8c8765721b5cb2907182a63c562677447df8caea (diff)
downloadscade-analyzer-0ce4cf6e7e280269db5da7c7b4fcb977b7f6f2cd.tar.gz
scade-analyzer-0ce4cf6e7e280269db5da7c7b4fcb977b7f6f2cd.zip
Warning for contradictory hypotheses was wrong.
-rw-r--r--abstract/abs_interp.ml28
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;