Module Flags.Certif

module Certif: sig .. end

Certificates and Proofs



type mink = [ `Auto | `Bwd | `Dicho | `FrontierDicho | `Fwd | `No ] 
Minimization stragegy for k
type mininvs = [ `Easy | `Hard | `HardOnly | `Medium | `MediumOnly ] 
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