sig
  module Make_Lazy_Model_Checker :
    functor (Abstraction : BlastArch.ABSTRACTION) ->
      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 = Abstraction.Operation.exp
                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 = 'a Abstraction.Region.coverers
                val emptyCoverers : unit -> 'a coverers
                val clearCoverers : 'a coverers -> unit
                val addCoverer : 'a coverers -> t -> 'a -> 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
        type error_path =
          Abstraction.Region.t * Abstraction.Operation.t list *
          Abstraction.Region.t
        and model_check_outcome =
          error_path BlastArch.ModelCheckOutcome.outcome
        val model_check_tar :
          Abstraction.Region.t ->
          Abstraction.Region.t option -> model_check_outcome
        val model_check :
          Abstraction.Region.t ->
          Abstraction.Region.t option -> model_check_outcome
        val print_stats : Format.formatter -> unit -> unit
        val print_phis : bool -> string
        val process_env_assumptions :
          (Ast.Expression.lval * Ast.Predicate.predicate) list -> unit
      end
end