why3bench man page

why3bench — 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).

0.87.2 why3 User Commands