diff options
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 2597a63..b5fc684 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -171,7 +171,7 @@ end = struct (* program expressions *) cl : conslist; - guarantees : (id * bool_expr) list; + guarantees : (id * bool_expr * id) list; (* abstract interpretation *) cycle : (id * id * typ) list; (* s'(x) = s(y) *) @@ -283,7 +283,7 @@ end = struct let guarantees = Transform.guarantees_of_prog rp 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 "@."; @@ -433,7 +433,7 @@ end = struct Format.printf "Accessible: %a@." print_dd final; - 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; |