why3 - Man Page

check verification conditions in source code


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 selected theories from the library.


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


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.


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


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


Set all debug flags except parse_only and type_only.

--debug <flag>

Set a debug flag.


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


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


Print version information.

-help,  --help

Show a list of options.

See Also

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

Referenced By

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