sig
  exception Not_implemented of Llvm.llvalue
  val sprint_exn : Llvm.llvalue -> string
  exception Variable_not_found of (bool * Llvm.llvalue)
  val sprint_exn_var : bool * Llvm.llvalue -> string
  exception Block_not_found of (bool * Llvm.llbasicblock)
  val sprint_exn_block : bool * Llvm.llbasicblock -> string
  module Init :
    functor
      (ZZ3 : ZZ3_sigs.S) (SMTg : sig
                                   type t = Smtgraph.Make(ZZ3).t
                                   module V :
                                     sig
                                       type t = Smtgraph.Make(ZZ3).V.t
                                       val compare : t -> t -> int
                                       val hash : t -> int
                                       val equal : t -> t -> bool
                                       type label =
                                           Smtgraph.Make(ZZ3).V.label
                                       val create : label -> t
                                       val label : t -> label
                                     end
                                   type vertex = V.t
                                   module E :
                                     sig
                                       type t = Smtgraph.Make(ZZ3).E.t
                                       val compare : t -> t -> int
                                       type vertex = vertex
                                       val src : t -> vertex
                                       val dst : t -> vertex
                                       type label = unit
                                       val create :
                                         vertex -> label -> vertex -> t
                                       val label : t -> label
                                     end
                                   type edge = E.t
                                   val is_directed : bool
                                   val is_empty : t -> bool
                                   val nb_vertex : t -> int
                                   val nb_edges : t -> int
                                   val out_degree : t -> vertex -> int
                                   val in_degree : t -> vertex -> int
                                   val mem_vertex : t -> vertex -> bool
                                   val mem_edge :
                                     t -> vertex -> vertex -> bool
                                   val mem_edge_e : t -> edge -> bool
                                   val find_edge :
                                     t -> vertex -> vertex -> edge
                                   val find_all_edges :
                                     t -> vertex -> vertex -> edge list
                                   val succ : t -> vertex -> vertex list
                                   val pred : t -> vertex -> vertex list
                                   val succ_e : t -> vertex -> edge list
                                   val pred_e : t -> vertex -> edge list
                                   val iter_vertex :
                                     (vertex -> unit) -> t -> unit
                                   val fold_vertex :
                                     (vertex -> 'a -> 'a) -> t -> 'a -> 'a
                                   val iter_edges :
                                     (vertex -> vertex -> unit) -> t -> unit
                                   val fold_edges :
                                     (vertex -> vertex -> 'a -> 'a) ->
                                     t -> 'a -> 'a
                                   val iter_edges_e :
                                     (edge -> unit) -> t -> unit
                                   val fold_edges_e :
                                     (edge -> 'a -> 'a) -> t -> 'a -> 'a
                                   val map_vertex :
                                     (vertex -> vertex) -> t -> t
                                   val iter_succ :
                                     (vertex -> unit) -> t -> vertex -> unit
                                   val iter_pred :
                                     (vertex -> unit) -> t -> vertex -> unit
                                   val fold_succ :
                                     (vertex -> 'a -> 'a) ->
                                     t -> vertex -> 'a -> 'a
                                   val fold_pred :
                                     (vertex -> 'a -> 'a) ->
                                     t -> vertex -> 'a -> 'a
                                   val iter_succ_e :
                                     (edge -> unit) -> t -> vertex -> unit
                                   val fold_succ_e :
                                     (edge -> 'a -> 'a) ->
                                     t -> vertex -> 'a -> 'a
                                   val iter_pred_e :
                                     (edge -> unit) -> t -> vertex -> unit
                                   val fold_pred_e :
                                     (edge -> 'a -> 'a) ->
                                     t -> vertex -> 'a -> 'a
                                   val empty : t
                                   val add_vertex : t -> vertex -> t
                                   val remove_vertex : t -> vertex -> t
                                   val add_edge : t -> vertex -> vertex -> t
                                   val add_edge_e : t -> edge -> t
                                   val remove_edge :
                                     t -> vertex -> vertex -> t
                                   val remove_edge_e : t -> edge -> t
                                   val get_clauses :
                                     V.t -> ZZ3.zbool ZZ3.term list
                                   val from_llvm :
                                     (Llvmcfg.vertex ->
                                      ZZ3.zbool ZZ3.term list) ->
                                     Llvmcfg.vertex -> vertex
                                   module Dot :
                                     sig
                                       val fprint_graph :
                                         Format.formatter -> t -> unit
                                       val output_graph :
                                         out_channel -> t -> unit
                                     end
                                   val to_smt : t -> [> ZZ3.zbool ] ZZ3.term
                                 end) ->
      sig
        val env : (Llvm.llvalue * bool, Z3.Expr.expr) Hashtbl.t
        val get_var : primed:bool -> Llvm.llvalue -> [> ZZ3.znum ] ZZ3.term
        val get_block :
          primed:bool -> Llvm.llbasicblock -> [> ZZ3.zbool ] ZZ3.term
        val llvm2smt :
          Llvm.llvalue -> Llvm.llbasicblock list -> Llvmcfg.t -> SMTg.t
      end
end