let system s = let l = init_global_env s in if not Options.notyping then init s.init; if Options.subtyping then Smt.Variant.init l; if not Options.notyping then List.iter unsafe s.unsafe; if not Options.notyping then List.iter unsafe (List.rev s.invs); if not Options.notyping then transitions s.trans; if Options.(subtyping && not murphi) then begin Smt.Variant.close (); if Options.debug then Smt.Variant.print (); end; let init_woloc = let _,v,i = s.init in v,i in let invs_woloc = List.map (fun (_,v,i) -> create_node_rename Inv v i) s.invs in let unsafe_woloc = List.map (fun (_,v,u) -> create_node_rename Orig v u) s.unsafe in let init_instances = create_init_instances init_woloc invs_woloc in if Options.debug && Options.verbose > 0 then debug_init_instances init_instances; { t_globals = List.map (fun (_,g,_) -> g) s.globals; t_consts = List.map (fun (_,c,_) -> c) s.consts; t_arrays = List.map (fun (_,a,_) -> a) s.arrays; t_init = init_woloc; t_init_instances = init_instances; t_invs = invs_woloc; t_unsafe = unsafe_woloc; t_trans = List.map add_tau s.trans; }