functor
  (Abstraction : sig
                   module Operation :
                     sig
                       type t
                       val print : Format.formatter -> t -> unit
                       val to_string : t -> string
                       type exp = Ast.Expression.expression
                       and lval
                       and info =
                           Normal
                         | Call of lval option * string * exp list
                         | Ret of exp
                       val get_info : t -> info
                     end
                   module Region : BlastArch.REGION
                   val reg_to_strings : Region.t -> string list * string
                   val reg_function_name : Region.t -> string
                   val reg_to_string : Region.t -> string
                   val op_to_string : Operation.t -> int * int * string
                   type phi_table =
                     (Ast.Expression.lval, Region.t ref) Hashtbl.t
                   val post :
                     Region.t -> Operation.t -> phi_table -> Region.t
                   val pre : Region.t -> Operation.t -> phi_table -> Region.t
                   val summary_post :
                     Operation.t ->
                     Region.t -> Region.t -> phi_table -> Region.t
                   val spre :
                     Region.t -> Operation.t -> phi_table -> Region.t
                   val erase_data : Region.t -> Region.t
                   val predicate_to_region :
                     Ast.Predicate.predicate -> Region.t
                   val create_concrete_true_region : Operation.t -> Region.t
                   val create_abstract_true_region : Operation.t -> Region.t
                   val trim_region_to_globals : Region.t -> Region.t
                   val new_name :
                     string -> Ast.Expression.lval -> Ast.Expression.lval
                   val brand_new_suffix : unit -> string
                   val assumed_invariants_region : Region.t ref
                   val precise : Region.t -> Region.t
                   exception NoNewPredicatesException
                   val focus : Region.t -> Region.t -> Region.t
                   val focus_stamp : Region.t -> Region.t
                   val analyze_trace :
                     Region.t list -> Operation.t list -> unit
                   val block_analyze_trace :
                     Region.t list ->
                     Operation.t list -> int list -> int * Region.t
                   val find_all_predicates :
                     Region.t list -> Operation.t list -> unit
                   val predicate_fixpoint_reached : unit -> bool
                   val coverable : Region.t -> bool
                   val covered : Region.t -> Region.t -> bool
                   val intersect_with_abstraction :
                     Region.t -> Region.t -> Region.t
                   val print_abs_stats : unit -> unit
                   val reset_abs_stats : unit -> unit
                   val enabled_ops : Region.t -> Operation.t list
                   val print_debug_info : Operation.t list -> unit
                   val isPredicate : Operation.t -> bool
                   val check_emptiness : Operation.t -> bool
                   val reset : unit -> unit
                   val can_escape : Ast.Expression.lval -> bool
                   val is_lock : Ast.Expression.lval -> bool
                   type proof_region
                   and lemma_index
                   val post_proof :
                     Region.t ->
                     Operation.t -> phi_table -> proof_region * lemma_index
                   val check_reg_eq : proof_region -> Region.t -> bool
                   val extract_proof_region : Region.t -> proof_region
                   val print_proof_region : proof_region -> unit
                   val print_proofTable : unit -> unit
                   val iter_global_variables :
                     (Ast.Expression.lval -> unit) -> unit
                   type access_type = Anone | Aread | Awrite | Aboth
                   val accessing :
                     Operation.t -> Ast.Expression.lval -> access_type
                   val get_all_writes :
                     Operation.t -> Ast.Expression.lval list
                   val get_all_reads :
                     Operation.t -> Ast.Expression.lval list
                   val reads_and_writes :
                     Operation.t ->
                     Ast.Expression.lval list * Ast.Expression.lval list
                   val aliasesOf :
                     Ast.Expression.lval -> Ast.Expression.lval list
                   val multiply_instantiable :
                     Region.t ->
                     Region.t ->
                     Ast.Expression.lval ->
                     Ast.Expression.lval -> Region.t option
                   val make_multiply_instantiable_region :
                     Region.t ->
                     Region.t ->
                     Ast.Expression.lval -> Ast.Expression.lval -> Region.t
                   type spec
                   and spec_result =
                       Yes
                     | No
                     | Maybe of Ast.Predicate.predicate
                   val init_spec : unit -> unit
                   val build_spec :
                     string -> (Region.t * Region.t list) list -> spec
                   val check_spec : spec -> spec -> spec_result
                   val predIndex : int ref
                 end->
  sig
    module Abstraction :
      sig
        module Operation :
          sig
            type t = Abstraction.Operation.t
            val print : Format.formatter -> t -> unit
            val to_string : t -> string
            type exp = Ast.Expression.expression
            and lval = Abstraction.Operation.lval
            and info =
              Abstraction.Operation.info =
                Normal
              | Call of lval option * string * exp list
              | Ret of exp
            val get_info : t -> info
          end
        module Region :
          sig
            type t = Abstraction.Region.t
            val print : Format.formatter -> t -> unit
            val to_string : t -> string
            val eq : t -> t -> bool
            val leq : t -> t -> bool
            val cup : t -> t -> t
            val cap : t -> t -> t
            val bot : t
            val is_empty : t -> bool
            val concretize : t -> t
            val rename_vars :
              t -> (Ast.Expression.lval -> Ast.Expression.lval) -> t
            val change_location_and_stack : t -> t -> t
            type 'a coverers = 'Abstraction.Region.coverers
            val emptyCoverers : unit -> 'a coverers
            val clearCoverers : 'a coverers -> unit
            val addCoverer : 'a coverers -> t -> '-> unit
            val findCoverer : 'a coverers -> t -> 'a option
            type restriction = Abstraction.Region.restriction
            val negate_restriction : restriction -> restriction
            val locals_and_globals : string -> restriction
            val only_globals : restriction
            val only_locals : string -> restriction
            val restrict : restriction -> t -> t
          end
        val reg_to_strings : Region.t -> string list * string
        val reg_function_name : Region.t -> string
        val reg_to_string : Region.t -> string
        val op_to_string : Operation.t -> int * int * string
        type phi_table = (Ast.Expression.lval, Region.t ref) Hashtbl.t
        val post : Region.t -> Operation.t -> phi_table -> Region.t
        val pre : Region.t -> Operation.t -> phi_table -> Region.t
        val summary_post :
          Operation.t -> Region.t -> Region.t -> phi_table -> Region.t
        val spre : Region.t -> Operation.t -> phi_table -> Region.t
        val erase_data : Region.t -> Region.t
        val predicate_to_region : Ast.Predicate.predicate -> Region.t
        val create_concrete_true_region : Operation.t -> Region.t
        val create_abstract_true_region : Operation.t -> Region.t
        val trim_region_to_globals : Region.t -> Region.t
        val new_name : string -> Ast.Expression.lval -> Ast.Expression.lval
        val brand_new_suffix : unit -> string
        val assumed_invariants_region : Region.t ref
        val precise : Region.t -> Region.t
        exception NoNewPredicatesException
        val focus : Region.t -> Region.t -> Region.t
        val focus_stamp : Region.t -> Region.t
        val analyze_trace : Region.t list -> Operation.t list -> unit
        val block_analyze_trace :
          Region.t list -> Operation.t list -> int list -> int * Region.t
        val find_all_predicates : Region.t list -> Operation.t list -> unit
        val predicate_fixpoint_reached : unit -> bool
        val coverable : Region.t -> bool
        val covered : Region.t -> Region.t -> bool
        val intersect_with_abstraction : Region.t -> Region.t -> Region.t
        val print_abs_stats : unit -> unit
        val reset_abs_stats : unit -> unit
        val enabled_ops : Region.t -> Operation.t list
        val print_debug_info : Operation.t list -> unit
        val isPredicate : Operation.t -> bool
        val check_emptiness : Operation.t -> bool
        val reset : unit -> unit
        val can_escape : Ast.Expression.lval -> bool
        val is_lock : Ast.Expression.lval -> bool
        type proof_region = Abstraction.proof_region
        and lemma_index = Abstraction.lemma_index
        val post_proof :
          Region.t -> Operation.t -> phi_table -> proof_region * lemma_index
        val check_reg_eq : proof_region -> Region.t -> bool
        val extract_proof_region : Region.t -> proof_region
        val print_proof_region : proof_region -> unit
        val print_proofTable : unit -> unit
        val iter_global_variables : (Ast.Expression.lval -> unit) -> unit
        type access_type =
          Abstraction.access_type =
            Anone
          | Aread
          | Awrite
          | Aboth
        val accessing : Operation.t -> Ast.Expression.lval -> access_type
        val get_all_writes : Operation.t -> Ast.Expression.lval list
        val get_all_reads : Operation.t -> Ast.Expression.lval list
        val reads_and_writes :
          Operation.t -> Ast.Expression.lval list * Ast.Expression.lval list
        val aliasesOf : Ast.Expression.lval -> Ast.Expression.lval list
        val multiply_instantiable :
          Region.t ->
          Region.t ->
          Ast.Expression.lval -> Ast.Expression.lval -> Region.t option
        val make_multiply_instantiable_region :
          Region.t ->
          Region.t -> Ast.Expression.lval -> Ast.Expression.lval -> Region.t
        type spec = Abstraction.spec
        and spec_result =
          Abstraction.spec_result =
            Yes
          | No
          | Maybe of Ast.Predicate.predicate
        val init_spec : unit -> unit
        val build_spec : string -> (Region.t * Region.t list) list -> spec
        val check_spec : spec -> spec -> spec_result
        val predIndex : int ref
      end
    module Region :
      sig
        type t = Abstraction.Region.t
        val print : Format.formatter -> t -> unit
        val to_string : t -> string
        val eq : t -> t -> bool
        val leq : t -> t -> bool
        val cup : t -> t -> t
        val cap : t -> t -> t
        val bot : t
        val is_empty : t -> bool
        val concretize : t -> t
        val rename_vars :
          t -> (Ast.Expression.lval -> Ast.Expression.lval) -> t
        val change_location_and_stack : t -> t -> t
        type 'a coverers = 'Abstraction.Region.coverers
        val emptyCoverers : unit -> 'a coverers
        val clearCoverers : 'a coverers -> unit
        val addCoverer : 'a coverers -> t -> '-> unit
        val findCoverer : 'a coverers -> t -> 'a option
        type restriction = Abstraction.Region.restriction
        val negate_restriction : restriction -> restriction
        val locals_and_globals : string -> restriction
        val only_globals : restriction
        val only_locals : string -> restriction
        val restrict : restriction -> t -> t
      end
    module Operation :
      sig
        type t = Abstraction.Operation.t
        val print : Format.formatter -> t -> unit
        val to_string : t -> string
        type exp = Ast.Expression.expression
        and lval = Abstraction.Operation.lval
        and info =
          Abstraction.Operation.info =
            Normal
          | Call of lval option * string * exp list
          | Ret of exp
        val get_info : t -> info
      end
    module Tree :
      sig
        type ('a, 'b) node = ('a, 'b) BiDirectionalLabeledTree.node
        and ('a, 'b) incoming_edge =
          ('a, 'b) BiDirectionalLabeledTree.incoming_edge
        val get_node_label : ('a, 'b) node -> 'a
        val get_parent_edge : ('a, 'b) node -> ('a, 'b) incoming_edge option
        val get_children : ('a, 'b) node -> ('a, 'b) node list
        val get_edge_label : ('a, 'b) incoming_edge -> 'b
        val get_source : ('a, 'b) incoming_edge -> ('a, 'b) node
        val get_parent : ('a, 'b) node -> ('a, 'b) node
        val set_node_label : ('a, 'b) node -> '-> unit
        val set_edge_label : ('a, 'b) incoming_edge -> '-> unit
        val has_parent : ('a, 'b) node -> bool
        val has_child : ('a, 'b) node -> bool
        val create_root : '-> ('a, 'b) node
        val create_child : '-> '-> ('a, 'b) node -> ('a, 'b) node
        val delete_children : ('a, 'b) node -> unit
        val delete_child : ('a, 'b) node -> unit
        val iter_descendants : ('-> unit) -> ('a, 'b) node -> unit
        val iter_ancestors : ('-> unit) -> ('a, 'b) node -> unit
        val fold_left_descendants :
          ('-> '-> 'a) -> '-> ('b, 'c) node -> 'a
        val fold_left_ancestors :
          ('-> '-> 'a) -> '-> ('b, 'c) node -> 'a
        val fold_right_descendants :
          ('-> '-> 'b) -> ('a, 'c) node -> '-> 'b
        val fold_right_ancestors :
          ('-> '-> 'b) -> ('a, 'c) node -> '-> 'b
        val count_nodes_descendants : ('a, 'b) node -> int
        val count_f_descendants :
          (('a, 'b) node -> bool) -> ('a, 'b) node -> int
        val node_depth : ('a, 'b) node -> int
        val path_to_root : ('a, 'b) node -> ('a, 'b) node list
        val subtree_depth : ('a, 'b) node -> int
        val traverse_bfs :
          (('a, 'b) node -> unit) ->
          (('a, 'b) node -> unit) -> ('a, 'b) node -> unit
      end
    type error_path =
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t *
      CfLazyModelChecker.Make_Lazy_Model_Checker.Operation.t list *
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t
    val fprintf : (unit, Format.formatter, unit) format -> unit
    val valOf : 'a option -> 'a
    module IntMap :
      sig
        type key = int
        and +'a t
        val empty : 'a t
        val add : key -> '-> 'a t -> 'a t
        val find : key -> 'a t -> 'a
        val remove : key -> 'a t -> 'a t
        val mem : key -> 'a t -> bool
        val iter : (key -> '-> unit) -> 'a t -> unit
        val map : ('-> 'b) -> 'a t -> 'b t
        val mapi : (key -> '-> 'b) -> 'a t -> 'b t
        val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      end
    type node_set =
      CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    and 'a node_map =
      (CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node * 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    and summary_path =
        ListPath of CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node list
      | ConsPath of CfLazyModelChecker.Make_Lazy_Model_Checker.summary_path *
          CfLazyModelChecker.Make_Lazy_Model_Checker.summary_path
    and pt_data = CfLazyModelChecker.Make_Lazy_Model_Checker.summary_path
    and entry_node = {
      mutable call_sites :
        CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t
        CfLazyModelChecker.Make_Lazy_Model_Checker.node_map;
      mutable exit_pts :
        CfLazyModelChecker.Make_Lazy_Model_Checker.pt_data
        CfLazyModelChecker.Make_Lazy_Model_Checker.node_map;
    } 
    and exit_node = {
      mutable entry_pts :
        CfLazyModelChecker.Make_Lazy_Model_Checker.pt_data
        CfLazyModelChecker.Make_Lazy_Model_Checker.node_map;
    } 
    and node_kind =
        Node
      | Entry of CfLazyModelChecker.Make_Lazy_Model_Checker.entry_node
      | Exit of CfLazyModelChecker.Make_Lazy_Model_Checker.exit_node
    and marking_data = {
      mutable time_stamp : int;
      mutable region : CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t;
      mutable call_time_stamp : int option;
    } 
    and marking =
        Unprocessed
      | Processed_Covered of
          CfLazyModelChecker.Make_Lazy_Model_Checker.marking_data
      | Processed_Uncovered of
          CfLazyModelChecker.Make_Lazy_Model_Checker.marking_data
      | Processed_Was_Covered_To_Reprocess of
          CfLazyModelChecker.Make_Lazy_Model_Checker.marking_data
    and node_data = {
      id : int;
      mutable mark : CfLazyModelChecker.Make_Lazy_Model_Checker.marking;
      kind : CfLazyModelChecker.Make_Lazy_Model_Checker.node_kind;
    } 
    and summary_data = {
      path : CfLazyModelChecker.Make_Lazy_Model_Checker.summary_path;
      n_in : CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node;
      n_out : CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node;
    } 
    and edge =
        SummaryEdge of
          CfLazyModelChecker.Make_Lazy_Model_Checker.summary_data
      | PathEdge of CfLazyModelChecker.Make_Lazy_Model_Checker.Operation.t
    and tree_node =
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
    and flat_tree_node =
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.Operation.t)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
    val print_marking_data :
      Format.formatter ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.marking_data -> unit
    val print_marking :
      Format.formatter ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.marking -> unit
    val print_marking_short :
      Format.formatter ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.marking -> unit
    val print_node_data :
      Format.formatter ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.node_data -> unit
    val print_option : ('-> unit) -> Format.formatter -> 'a option -> unit
    val print_node :
      Format.formatter ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> unit
    val tree_node_table :
      (int,
       CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node Pervasives.ref)
      Hashtbl.t
    val get_node_data :
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> 'a
    val edge_to_op :
      CfLazyModelChecker.Make_Lazy_Model_Checker.edge ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Operation.t
    val get_edge_op :
      ('a, CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.incoming_edge ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Operation.t
    val get_op :
      ('a, CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Operation.t
    val get_parent :
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
    val get_parent_edge :
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> 'b
    val get_children :
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node list
    val get_id :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> int
    val get_marking :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.marking
    val get_marking_data :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.marking_data
    val get_time_stamp :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> int
    val min : '-> '-> 'a
    val max : '-> '-> 'a
    val update_caller :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      int option -> unit
    val called_after :
      CfLazyModelChecker.Make_Lazy_Model_Checker.marking_data -> int -> bool
    val print_tree_node :
      Format.formatter ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> unit
    val node_equal :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> bool
    val get_kind :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.node_kind
    val get_entry :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.entry_node
    val get_exit :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.exit_node
    val get_region :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t
    val get_region_opt :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t option
    type nset =
      CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nset_empty : 'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nset_add :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nset_mem :
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> bool
    val nset_remove :
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nset_iter :
      ('-> unit) ->
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t -> unit
    val nset_map :
      ('-> 'b) ->
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      ('-> 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nset_fold :
      ('-> '-> 'a) ->
      '-> 'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t -> 'a
    val nset_choose :
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t -> 'a option
    val nset_filter :
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> bool) ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nset_join :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nset_to_list :
      CfLazyModelChecker.Make_Lazy_Model_Checker.node_set ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node list
    val nset_size :
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t -> int
    val nmap_empty : 'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nmap_add :
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node * 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      '->
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node * 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nmap_mem :
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> bool
    val nmap_remove :
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nmap_iter :
      ('-> '-> unit) ->
      ('a * 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t -> unit
    val nmap_map :
      ('-> 'b) ->
      'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      ('d * '-> 'd * 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nmap_fold :
      ('-> '-> '-> 'a) ->
      '->
      ('b * 'c) CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t -> 'a
    val nmap_filter :
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> '-> bool) ->
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node * 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node * 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nmap_join :
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node * 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node * 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node * 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val nmap_to_list :
      CfLazyModelChecker.Make_Lazy_Model_Checker.pt_data
      CfLazyModelChecker.Make_Lazy_Model_Checker.node_map ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node *
       CfLazyModelChecker.Make_Lazy_Model_Checker.pt_data)
      list
    val nmap_size :
      ('a * 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t -> int
    val nmap_isEmpty :
      ('a * 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t -> bool
    val nmap_choose :
      ('-> bool) ->
      ('b * 'a) CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t ->
      'b option
    class tree_node_creator :
      object
        val mutable next_id : int
        method create_child :
          CfLazyModelChecker.Make_Lazy_Model_Checker.node_kind ->
          CfLazyModelChecker.Make_Lazy_Model_Checker.marking ->
          CfLazyModelChecker.Make_Lazy_Model_Checker.edge ->
          (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
           CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
          CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
          CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node
        method create_root :
          CfLazyModelChecker.Make_Lazy_Model_Checker.marking ->
          CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node
        method delete_children :
          CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node -> unit
      end
    val entry_pts_node :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
        CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node *
       CfLazyModelChecker.Make_Lazy_Model_Checker.summary_path)
      list
    val single_child :
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
    val single_child_edge :
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> 'b
    val parent_edge :
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> 'b
    val tlSafe : 'a list -> 'a list
    val exit_pts_node :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
        CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node *
       CfLazyModelChecker.Make_Lazy_Model_Checker.summary_path)
      list
    exception RestartException
    val stats_nb_iterations : int Pervasives.ref
    val stats_nb_iterations_of_outer_loop : int Pervasives.ref
    val stats_nb_created_nodes : int Pervasives.ref
    val stats_nb_refinment_processes : int Pervasives.ref
    val stats_nb_refined_nodes : int Pervasives.ref
    val stats_nb_proof_tree_nodes : int Pervasives.ref
    val stats_nb_proof_tree_covered_nodes : int Pervasives.ref
    val stats_nb_deleted_nodes : int Pervasives.ref
    val reset_stats : unit
    val print_stats : Format.formatter -> unit -> unit
    type 'a outcome =
      'BlastArch.ModelCheckOutcome.outcome =
        No_error
      | Error_reached of 'a
      | Race_condition of 'a * 'a * Ast.Expression.lval * Ast.Expression.lval
      | Bad_lock_spec of 'a * Ast.Expression.lval
    and model_check_outcome =
      CfLazyModelChecker.Make_Lazy_Model_Checker.error_path outcome
    exception Exit_from_check_concurrent_access of
                CfLazyModelChecker.Make_Lazy_Model_Checker.model_check_outcome
    type 'a currentApproximation = {
      read_whole : CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t;
      write_whole : CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t;
      read_accesses :
        ('a * CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t) list;
      write_accesses :
        ('a * CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t) list;
    } 
    and raceKind = Read | Write | Both | NoDistinction
    exception RaceConditionException of
                CfLazyModelChecker.Make_Lazy_Model_Checker.model_check_outcome
    val global_variable_table :
      CfLazyModelChecker.Make_Lazy_Model_Checker.Abstraction.phi_table
    val iter_global_variables :
      (Ast.Expression.lval ->
       CfLazyModelChecker.Make_Lazy_Model_Checker.Abstraction.Region.t
       Pervasives.ref -> unit) ->
      unit
    val get_global_var_phi :
      Ast.Expression.lval ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Abstraction.Region.t
      Pervasives.ref
    val global_lock_asm_table :
      (Ast.Expression.lval,
       CfLazyModelChecker.Make_Lazy_Model_Checker.Abstraction.Region.t)
      Hashtbl.t
    val process_env_assumptions :
      (Ast.Expression.lval * Ast.Predicate.predicate) list -> unit
    val print_phis : bool -> string
    type error_check =
        EmptyErrorAtNode of
          CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t *
          CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node *
          CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node list *
          CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node list
      | NonEmptyErrorAtRoot of
          CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t *
          CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node *
          CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node list
    val is_entry :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'a)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> bool
    val get_outgoing :
      ('a, CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Operation.t
    val expand_summary_path :
      CfLazyModelChecker.Make_Lazy_Model_Checker.summary_path ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node list
    val expand_path_with_old :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node list ->
      ((CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
        CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node list
    val expand_path :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node list ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node list
    val path_to_root :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node list
    val check_error :
      CfLazyModelChecker.Make_Lazy_Model_Checker.tree_node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.error_check
    val refine_path :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node list -> unit
    val add_pt :
      ('a,
       (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'b)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
       CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t)
      Hashtbl.t ->
      '->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'b)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> unit
    val has_pt :
      ('a, 'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t) Hashtbl.t ->
      '->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'c)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> bool
    val remove_pt :
      ('a, 'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t) Hashtbl.t ->
      '->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data, 'c)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> unit
    val clear_pts : ('a, 'b) Hashtbl.t -> unit
    val get_pts :
      ('a, 'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t) Hashtbl.t ->
      '-> 'CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t
    val iter_pts : ('-> '-> unit) -> ('a, 'b) Hashtbl.t -> unit
    val print_summaries :
      Format.formatter ->
      (string,
       (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
        CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
       CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t)
      Hashtbl.t -> unit
    val update_tree_after_refinment :
      (string,
       (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
        CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
       CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
       CfLazyModelChecker.Make_Lazy_Model_Checker.IntMap.t)
      Hashtbl.t ->
      < add_element : (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
                       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
                      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
                      unit;
        .. > ->
      int ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.coverers -> unit
    type proof_tree_node_data = {
      pt_id : int;
      pt_region :
        CfLazyModelChecker.Make_Lazy_Model_Checker.Abstraction.proof_region;
      covering_nodes :
        (CfLazyModelChecker.Make_Lazy_Model_Checker.Abstraction.lemma_index *
         CfLazyModelChecker.Make_Lazy_Model_Checker.proof_tree_node
         Pervasives.ref list)
        option;
    } 
    and proof_tree_edge =
      CfLazyModelChecker.Make_Lazy_Model_Checker.Operation.t *
      CfLazyModelChecker.Make_Lazy_Model_Checker.Abstraction.lemma_index
    and proof_tree_node =
      (CfLazyModelChecker.Make_Lazy_Model_Checker.proof_tree_node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.proof_tree_edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node
    val print_proof_tree :
      CfLazyModelChecker.Make_Lazy_Model_Checker.proof_tree_node -> unit
    val count_tree_nodes :
      ('a, 'b) CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> unit
    val build_proof_tree :
      unit ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node -> unit
    val dumptrace :
      'a *
      CfLazyModelChecker.Make_Lazy_Model_Checker.Abstraction.Operation.t list *
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t list -> unit
    val dumppath :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t -> unit
    val dump_trace_to_node :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t -> '-> unit
    val demo_process :
      (CfLazyModelChecker.Make_Lazy_Model_Checker.node_data,
       CfLazyModelChecker.Make_Lazy_Model_Checker.edge)
      CfLazyModelChecker.Make_Lazy_Model_Checker.Tree.node ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t -> bool -> unit
    val model_check :
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t ->
      CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t option ->
      (CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t *
       CfLazyModelChecker.Make_Lazy_Model_Checker.Operation.t list *
       CfLazyModelChecker.Make_Lazy_Model_Checker.Region.t)
      outcome
  end