module type S =sig..end
The interface of certificate generators
val certificate : Ast.t_system -> Node.t list -> unitthis takes a system in input and the list of visited nodes, of which the disjunction constitutes an inductive invariant for the system.
certificate s visited must write on the disk a certificate of induction
(initialization, preservation, and implication) and print the location
of the generated certificate on stdout.