sig
  val apply_after_transformation : Project.t -> unit
  val mv_invariants : Env.t -> old:Cil_types.stmt -> Cil_types.stmt -> unit
  val preserve_invariant :
    Project.t ->
    Env.t ->
    Kernel_function.t -> Cil_types.stmt -> Cil_types.stmt * Env.t * bool
  val mk_nested_loops :
    loc:Cil_types.location ->
    (Env.t -> Cil_types.stmt list * Env.t) ->
    Cil_types.kernel_function ->
    Env.t -> Lscope.lscope_var list -> Cil_types.stmt list * Env.t
  val translate_named_predicate_ref :
    (Cil_types.kernel_function -> Env.t -> Cil_types.predicate -> Env.t)
    Pervasives.ref
  val named_predicate_ref :
    (Cil_types.kernel_function ->
     Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
    Pervasives.ref
  val term_to_exp_ref :
    (Cil_types.kernel_function ->
     Env.t -> Cil_types.term -> Cil_types.exp * Env.t)
    Pervasives.ref
end