why3 man page

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

Verify conditions in source code.  If the filename is "-", then input is read from stdin.

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

Prove or print (with -o) the selected goals using prover.

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

-D, --driver <file>

Specify a prover's driver (conflicts with -P).

-o, --output <dir>

Print the selected goals to separate files in dir.

--realize

Realize selected theories from the library.

--bisect

Reduce the set of needed axioms which prove a goal, and output the resulting task.

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

--parse-only

Stop after parsing (same as --debug parse_only).

--type-only

Stop after type checking (same as --debug type_only).

--debug-all

Set all debug flags except parse_only and type_only.

--debug <flag>

Set a debug flag.

--print-libdir

Print location of binary components (plugins, etc.).

--print-datadir

Print location of non-binary data (theories, modules, etc.).

--version

Print version information.

-help, --help

Show a list of options.

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

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