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