1WHY3BENCH(1)                     User Commands                    WHY3BENCH(1)
2
3
4

NAME

6       why3bench - schedule verification checking
7

SYNOPSIS

9       why3bench [OPTIONS] [[FILE|-] [-T <theory> [-G <goal>] ... ] ... ]
10

DESCRIPTION

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

OPTIONS

18       -T, --theory <theory>
19              Select theory in the input file or in the library.
20
21       -G, --goal <goal>
22              Select goal in the last selected theory.
23
24       -C, --config <file>
25              Read configuration from file.
26
27       -L, --library <dir>
28              Add dir to the library search path.
29
30       -P, --prover <prover>
31              Add prover in the bench.
32
33       -B <bench>
34              Read one bench configuration file from bench.
35
36       -d <dir>
37              Specify the directory containing the database.
38
39       --redo-db
40              Check that the proof attempts in the database (-d) give the same
41              results.
42
43       -F, --format <format>
44              Select the input format (default: "why").
45
46       -t, --timelimit <sec>
47              Set  the  prover's time limit in seconds, where 0 means no limit
48              (default: 10).
49
50       -m, --memlimit <MiB>
51              Set the prover's memory limit in megabytes (default: no limit).
52
53       -a, --apply-transform <transformation>
54              Apply a transformation to every task.
55
56       -M, --meta <metaname>=<string>
57              Add a string meta to every task.
58
59       -o, --output <dir>
60              Print the selected goals to separate files in dir.
61
62       --print-theory
63              Print selected theories.
64
65       --print-namespace
66              Print namespaces of selected theories.
67
68       --list-transforms
69              List known transformations.
70
71       --list-printers
72              List known printers.
73
74       --list-provers
75              List known provers.
76
77       --list-formats
78              List known input formats.
79
80       --list-metas
81              List known metas.
82
83       --list-debug-flags
84              List known debug flags.
85
86       --debug-all
87              Set all debug flags except parse_only and type_only.
88
89       --debug <flag>
90              Set a debug flag.
91
92       --quiet
93              Print only explicitly requested information.
94
95       --version
96              Print version information.
97
98       -help, --help
99              Show a list of options.
100

SEE ALSO

102       why3(1),  why3-cpulimit(1),  why3config(1),   why3doc(1),   why3ide(1),
103       why3ml(1), why3realize(1), why3replayer(1)
104
105
106
107why3                                 1.1.1                        WHY3BENCH(1)
Impressum