https://github.com/EasyCrypt/easycrypt
Revision de0e2402092bf115a0e548ed4bcc0d5e0d351cb6 authored by Pierre-Yves Strub on 20 April 2018, 05:14:36 UTC, committed by Pierre-Yves Strub on 21 April 2018, 20:20:39 UTC
This option expects an integer argument. It indicates the number
of smt provers that must solve a goal before being accepted.

A value of 0 set the quorum to its default value (1).

Note that if provers do not agree while waiting to reach a
quorum, the goal is rejected.

[closes #17371]
1 parent 6ffe960
Raw File
Tip revision: de0e2402092bf115a0e548ed4bcc0d5e0d351cb6 authored by Pierre-Yves Strub on 20 April 2018, 05:14:36 UTC
New smt option: quorum
Tip revision: de0e240
ecFortune.mli
(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2018 - Inria
 * Copyright (c) - 2012--2018 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-C-V1 license
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
val init : unit -> unit
val pick : unit -> string option
back to top