why3bench - Man Page

schedule verification checking

Synopsis

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

Description

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.

Options

-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.

--redo-db

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-theory

Print selected theories.

--print-namespace

Print namespaces of selected theories.

--list-transforms

List known transformations.

--list-printers

List known printers.

--list-provers

List known provers.

--list-formats

List known input formats.

--list-metas

List known metas.

--list-debug-flags

List known debug flags.

--debug-all

Set all debug flags except parse_only and type_only.

--debug <flag>

Set a debug flag.

--quiet

Print only explicitly requested information.

--version

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