verification.mli

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(**************************************************************************)

val verify :
  ?debug:bool ->
  string option ->
  string list ->
  ?memlimit:int ->
  ?timeout:int ->
  Prover.t ->
  string ->
  unit
(** [verify debug format loadpath memlimit prover file] launches a verification
    of the given [file] with the provided [prover].

    @param debug when set, enables debug information.
    @param format is the [file] format.
    @param loadpath is the additional loadpath.
    @param memlimit
      is the memory limit (in megabytes) granted to the verification.
    @param timeout is the timeout (in seconds) granted to the verification. *)