Module Flags.Certif

Certificates and Proofs

type mink = [
  1. | `No
  2. | `Fwd
  3. | `Bwd
  4. | `Dicho
  5. | `FrontierDicho
  6. | `Auto
]

Minimization stragegy for k

type mininvs = [
  1. | `Easy
  2. | `Medium
  3. | `MediumOnly
  4. | `Hard
  5. | `HardOnly
]

Minimization stragegy for invariants

val certif : unit -> bool

Certification only.

val certif_slicing : unit -> bool

Certification only.

val proof : unit -> bool

Proof production.

val mink : unit -> mink

Minimization stragegy for k

val mininvs : unit -> mininvs

Minimization stragegy for invariants

val jkind_bin : unit -> string

Binary for JKind

val only_user_candidates : unit -> bool