type witness = {
  case : Syntax.t;
  model : Syntax.model;
  bound : int;
  fences : Syntax.location list;
  actors : int array;
}
type result = { witness : witness option; query : Solver.query }
type phase = Searching of int * Syntax.location list
  | Counterexample of witness | Excluded of int | Refining of int
  | Verified of Syntax.location list * int * int
type repair = {
  case : Syntax.t;
  fences : Syntax.location list;
  clauses : int list list;
  rounds : int;
  bound : int;
  states : int;
}
val check : ?timeout:int -> ?tick:(unit -> unit) -> ?bound:int ->
  ?fences:Syntax.location list -> ?folder:string -> ?fixed:int array ->
  Syntax.t -> Syntax.model -> result
val witness_sexp : witness -> Sexp.t
val load_witness : string -> witness
val replay : witness -> Machine.t array * Machine.event array
val save : string -> result -> unit
val repair : ?timeout:int -> ?tick:(unit -> unit) -> ?notify:(phase -> unit) ->
  Syntax.t -> string -> repair option
val load_repair : string -> repair
val certify : ?timeout:int -> ?tick:(unit -> unit) -> string -> repair
val audit : ?timeout:int -> ?tick:(unit -> unit) -> string -> string -> repair
val validate_schedule : ?timeout:int -> Syntax.t -> Syntax.location list -> int array -> unit
val outcomes : ?timeout:int -> ?tick:(unit -> unit) -> Syntax.t -> Syntax.model -> (int64 * int64) list