sig
  val get_uid : unit -> int
  type assumptions = Invs.t Scope.Map.t
  val assumptions_empty : Analysis.assumptions
  val assumptions_merge :
    Analysis.assumptions -> Analysis.assumptions -> Analysis.assumptions
  val assumptions_of_sys : TransSys.t -> Analysis.assumptions
  val assumptions_fold :
    ('-> Scope.t -> Invs.t -> 'a) -> '-> Analysis.assumptions -> 'a
  type info = {
    top : Scope.t;
    uid : int;
    abstraction_map : bool Scope.Map.t;
    assumptions : Analysis.assumptions;
  }
  val shrink_info_to_sys : Analysis.info -> TransSys.t -> Analysis.info
  type param =
      ContractCheck of Analysis.info
    | First of Analysis.info
    | Refinement of Analysis.info * Analysis.result
  and result = {
    param : Analysis.param;
    time : float;
    sys : TransSys.t;
    contract_valid : bool option;
    requirements_valid : bool option;
  }
  val info_clone : Analysis.info -> Analysis.info
  val param_clone : Analysis.param -> Analysis.param
  val info_of_param : Analysis.param -> Analysis.info
  val shrink_param_to_sys : Analysis.param -> TransSys.t -> Analysis.param
  val param_scope_is_abstract : Analysis.param -> Scope.t -> bool
  val param_assumptions_of_scope : Analysis.param -> Scope.t -> Invs.t
  val mk_result : Analysis.param -> TransSys.t -> float -> Analysis.result
  val result_is_all_proved : Analysis.result -> bool
  val result_is_some_falsified : Analysis.result -> bool
  type results
  val mk_results : unit -> Analysis.results
  val results_add : Analysis.result -> Analysis.results -> Analysis.results
  val results_find : Scope.t -> Analysis.results -> Analysis.result list
  val results_last : Scope.t -> Analysis.results -> Analysis.result
  val results_length : Analysis.results -> int
  val results_is_safe : Analysis.results -> bool option
  val results_clean : Analysis.results -> Analysis.results
  val pp_print_param : bool -> Format.formatter -> Analysis.param -> unit
  val pp_print_result_quiet : Format.formatter -> Analysis.result -> unit
  val pp_print_result : Format.formatter -> Analysis.result -> unit
end