diff options
Diffstat (limited to 'abstract/abs_interp_edd.ml')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index bff8e2b..31fe5aa 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -589,7 +589,7 @@ end = struct (* program expressions *) init_cl : conslist; cl : conslist; - guarantees : (id * bool_expr) list; + guarantees : (id * bool_expr * id) list; } @@ -801,7 +801,7 @@ end = struct let rp = { rp with all_vars = List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in - let repls = (repl, keep; "L"^repl, "L"^keep):: + let repls = [repl, keep; "L"^repl, "L"^keep]@ (List.map (fun (r, k) -> r, if k = repl then keep else @@ -829,10 +829,10 @@ end = struct let guarantees = Transform.guarantees_of_prog rp in let guarantees = List.map - (fun (id, f) -> id, formula_replace_evars repls f) + (fun (id, f, v) -> id, formula_replace_evars repls f, v) guarantees in Format.printf "Guarantees:@."; - List.iter (fun (id, f) -> + List.iter (fun (id, f, _) -> Format.printf " %s: %a@." id Formula_printer.print_expr f) guarantees; Format.printf "@."; @@ -936,7 +936,7 @@ end = struct Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final; (* Check guarantees *) - let check_guarantee (id, f) = + let check_guarantee (id, f, _) = let cl = Formula.conslist_of_f f in Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ " id Formula_printer.print_conslist cl; |