Module Flags.Certif

Certificates and Proofs

type mink = [
| `No
| `Fwd
| `Bwd
| `Dicho
| `FrontierDicho
| `Auto
]

Minimization stragegy for k

type mininvs = [
| `Easy
| `Medium
| `MediumOnly
| `Hard
| `HardOnly
]

Minimization stragegy for invariants

val certif : unit -> bool

Certification only.

val proof : unit -> bool

Proof production.

val abstr : unit -> bool

Use abstract type indexes in certificates/proofs.

val log_trust : unit -> bool

Log trusted parts of proofs.

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