why3bench - Man Page

schedule verification checking


why3bench [Options] [[FILE|-] [-T <theory> [-G <goal>] ... ] ... ]


The why3bench tool adds a scheduler on top of the Why3 library.  It is designed to compare various components of automatic proofs: automatic provers, transformations, and definitions of a theory.  For that goal, it tries to prove predefined goals using each component to compare.


-T,  --theory <theory>

Select theory in the input file or in the library.

-G,  --goal <goal>

Select goal in the last selected theory.

-C,  --config <file>

Read configuration from file.

-L,  --library <dir>

Add dir to the library search path.

-P,  --prover <prover>

Add prover in the bench.

-B <bench>

Read one bench configuration file from bench.

-d <dir>

Specify the directory containing the database.


Check that the proof attempts in the database (-d) give the same results.

-F,  --format <format>

Select the input format (default: "why").

-t,  --timelimit <sec>

Set the prover's time limit in seconds, where 0 means no limit (default: 10).

-m,  --memlimit <MiB>

Set the prover's memory limit in megabytes (default: no limit).

-a,  --apply-transform <transformation>

Apply a transformation to every task.

-M,  --meta <metaname>=<string>

Add a string meta to every task.

-o,  --output <dir>

Print the selected goals to separate files in dir.


Print selected theories.


Print namespaces of selected theories.


List known transformations.


List known printers.


List known provers.


List known input formats.


List known metas.


List known debug flags.


Set all debug flags except parse_only and type_only.

--debug <flag>

Set a debug flag.


Print only explicitly requested information.


Print version information.

-help,  --help

Show a list of options.

See Also

why3(1), why3-cpulimit(1), why3config(1), why3doc(1), why3ide(1), why3ml(1), why3realize(1), why3replayer(1)

Referenced By

why3(1), why3config(1), why3-cpulimit(1), why3doc(1), why3ide(1), why3ml(1), why3realize(1), why3replayer(1).

1.3.3 why3