Project

General

Profile

Revision 8c934ccd src/tools/seal/seal_verifier.ml

View differences:

src/tools/seal/seal_verifier.ml
60 60
  let sliced_nd = slice_node mems msch nd in
61 61
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
62 62
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
63
  let sw_init, sw_sys = node_as_switched_sys mems sliced_nd in
63

  
64
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
65
  let sw_init, sw_sys = node_as_switched_sys consts mems sliced_nd in
64 66
  let pp_res =
65 67
    (Utils.fprintf_list ~sep:"@ "
66 68
       (fun fmt (gel, up) ->

Also available in: Unified diff