Use 'dafny --help' to see help for a newer Dafny CLI format.
Usage: Dafny [ option ... ] [ filename ... ]
---- General options -------------------------------------------------------
/version print the Dafny version number
/help print this message
/attrHelp print a message about supported declaration attributes
/env:<n> print command line arguments
0 - never, 1 (default) - during BPL print and prover log,
2 - like 1 and also to standard output
/printVerifiedProceduresCount:<n>
0 - no
1 (default) - yes
/wait await Enter from keyboard before terminating program
/xml:<file> also produce output in XML format to <file>
All the .dfy files supplied on the command line along with files recursively
included by 'include' directives are considered a single Dafny program;
however only those files listed on the command line are verified.
Exit code: 0 -- success; 1 -- invalid command-line; 2 -- parse or type errors;
3 -- compilation errors; 4 -- verification errors
---- Input configuration ---------------------------------------------------
/dprelude:<file>
Choose the Dafny prelude file.
/stdin
Read standard input and treat it as an input .dfy file.
---- Plugins ---------------------------------------------------------------
/plugin:<path-to-one-assembly[,argument]*>
(experimental) One path to an assembly that contains at least one
instantiatable class extending Microsoft.Dafny.Plugin.Rewriter. It
can also extend Microsoft.Dafny.Plugins.PluginConfiguration to
receive arguments. More information about what plugins do and how
to define them:
https://github.com/dafny-lang/dafny/blob/master/Source/DafnyLanguageServer/README.md#about-plugins
---- Overall reporting and printing ----------------------------------------
/dprint:<file>
Print Dafny program after parsing it.
(Use - as <file> to print to console.)
/printMode:<Everything|DllEmbed|NoIncludes|NoGhost>
Everything (default) - Print everything listed below.
DllEmbed - print the source that will be included in a compiled dll.
NoIncludes - disable printing of {:verify false} methods
incorporated via the include mechanism, as well as datatypes and
fields included from other files.
NoGhost - disable printing of functions, ghost methods, and proof
statements in implementation methods. It also disables anything
NoIncludes disables.
/rprint:<file>
Print Dafny program after resolving it.
(use - as <file> to print to console.)
/showSnippets:<value>
0 (default) - Don't show source code snippets for Dafny messages.
1 - Show a source code snippet for each Dafny message.
/stats
Print interesting statistics about the Dafny files supplied.
/printIncludes:<None|Immediate|Transitive>
None (default) - Print nothing.
Immediate - Print files included by files listed on the command line.
Transitive - Recurses on the files printed by Immediate.
Immediate and Transitive will exit after printing.
/view:<view1, view2>
Print the filtered views of a module after it is resolved (/rprint).
If print before the module is resolved (/dprint), then everything in
the module is printed. If no view is specified, then everything in
the module is printed.
/funcCallGraph
Print out the function call graph. Format is: func,mod=callee*
/pmtrace
Print pattern-match compiler debug info.
/titrace
Print type-inference debug info.
/printTooltips
Dump additional positional information (displayed as mouse-over
tooltips by the VS Code plugin) to stdout as 'Info' messages.
/diagnosticsFormat:<text|json>
Choose how to report errors, warnings, and info messages.
text (default) - Use human readable output
json - Print each message as a JSON object, one per line.
---- Language feature selection --------------------------------------------
/unicodeChar:<value>
0 (default) - The char type represents any UTF-16 code unit.
1 - The char type represents any Unicode scalar value.
/noIncludes
Ignore include directives.
/noExterns
Ignore extern and dllimport attributes.
/functionSyntax:<version>
The syntax for functions is changing from Dafny version 3 to version
4. This switch gives early access to the new syntax, and also
provides a mode to help with migration.
3 (default) - Compiled functions are written `function method` and
`predicate method`. Ghost functions are written `function` and
`predicate`.
4 - Compiled functions are written `function` and `predicate`. Ghost
functions are written `ghost function` and `ghost predicate`.
migration3to4 - Compiled functions are written `function method` and
`predicate method`. Ghost functions are written `ghost function`
and `ghost predicate`. To migrate from version 3 to version 4,
use this flag on your version 3 program. This will give flag all
occurrences of `function` and `predicate` as parsing errors.
These are ghost functions, so change those into the new syntax
`ghost function` and `ghost predicate`. Then, start using
/functionSyntax:4. This will flag all occurrences of `function
method` and `predicate method` as parsing errors. So, change
those to just `function` and `predicate`. Now, your program uses
version 4 syntax and has the exact same meaning as your previous
version 3 program.
experimentalDefaultGhost - Like migration3to4, but allow `function`
and `predicate` as alternatives to declaring ghost functions and
predicates, respectively.
experimentalDefaultCompiled - Like migration3to4, but allow
`function` and `predicate` as alternatives to declaring compiled
functions and predicates, respectively.
experimentalPredicateAlwaysGhost - Compiled functions are written
`function`. Ghost functions are written `ghost function`.
Predicates are always ghost and are written `predicate`.
/quantifierSyntax:<version>
The syntax for quantification domains is changing from Dafny version
3 to version 4, more specifically where quantifier ranges (|
<Range>) are allowed. This switch gives early access to the new
syntax.
3 (default) - Ranges are only allowed after all quantified variables
are declared. (e.g. set x, y | 0 <= x < |s| && y in s[x] && 0 <=
y :: y)
4 - Ranges are allowed after each quantified variable declaration.
(e.g. set x | 0 <= x < |s|, y <- s[x] | 0 <= y :: y)
Note that quantifier variable domains (<- <Domain>) are available in
both syntax versions.
/disableScopes
Treat all export sets as 'export reveal *'. i.e. don't hide function
bodies or type definitions during translation.
/allowGlobals
Allow the implicit class '_default' to contain fields, instance
functions, and instance methods. These class members are declared at
the module scope, outside of explicit classes. This command-line
option is provided to simplify a transition from the behavior in the
language prior to version 1.9.3, from which point onward all
functions and methods declared at the module scope are implicitly
static and fields declarations are not allowed at the module scope.
---- Warning selection -----------------------------------------------------
/warnShadowing
Emits a warning if the name of a declared variable caused another
variable to be shadowed.
/warnMissingConstructorParenthesis
Emits a warning when a constructor name in a case pattern is not
followed by parentheses.
/deprecation:<n>
0 - Don't give any warnings about deprecated features.
1 (default) - Show warnings about deprecated features.
2 - Also point out where there's new simpler syntax.
/warningsAsErrors
Treat warnings as errors.
---- Verification options -------------------------------------------------
/dafnyVerify:<n>
0 - Stop after resolution and typechecking.
1 - Continue on to verification and compilation.
/verifyAllModules
Verify modules that come from an include directive.
/separateModuleOutput
Output verification results for each module separately, rather than
aggregating them after they are all finished.
/verificationLogger:<configuration string>
Logs verification results to the given test result logger. The
currently supported loggers are `trx`, `csv`, and `text`. These are
the XML-based format commonly used for test results for .NET
languages, a custom CSV schema, and a textual format meant for human
consumption. You can provide configuration using the same string
format as when using the --logger option for dotnet test, such as:
/verificationLogger:trx;LogFileName=<...>.
The exact mapping of verification concepts to these formats is
experimental and subject to change!
The `trx` and `csv` loggers automatically choose an output file name
by default, and print the name of this file to the console. The
`text` logger prints its output to the console by default, but can
send output to a file given the `LogFileName` option.
The `text` logger also includes a more detailed breakdown of what
assertions appear in each assertion batch. When combined with the
`/vcsSplitOnEveryAssert` option, it will provide approximate time
and resource use costs for each assertion, allowing identification
of especially expensive assertions.
/mimicVerificationOf:<Dafny version>
Let Dafny attempt to mimic the verification as it was in a previous
version of Dafny. Useful during migration to a newer version of
Dafny when a Dafny program has proofs, such as methods or lemmas,
that are unstable in the sense that their verification may become
slower or fail altogether after logically irrelevant changes are
made in the verification input.
Accepted versions are: 3.3 (note that this turns off features that
prevent classes of verification instability)
/noCheating:<n>
0 (default) - Allow assume statements and free invariants.
1 - Treat all assumptions as asserts, and drop free.
/induction:<n>
0 - Never do induction, not even when attributes request it.
1 - Only apply induction when attributes request it.
2 - Apply induction as requested (by attributes) and also for
heuristically chosen quantifiers.
3 - Apply induction as requested, and for heuristically chosen
quantifiers and lemmas.
4 (default) - Apply induction as requested, and for lemmas.
/inductionHeuristic:<n>
0 - Least discriminating induction heuristic (that is, lean toward
applying induction more often).
1,2,3,4,5 - Levels in between, ordered as follows as far as how
discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6.
6 (default) - Most discriminating.
/trackPrintEffects:<n>
0 (default) - Every compiled method, constructor, and iterator,
whether or not it bears a {:print} attribute, may have print
effects.
1 - A compiled method, constructor, or iterator is allowed to have
print effects only if it is marked with {:print}.
/allocated:<n>
Specify defaults for where Dafny should assert and assume
allocated(x) for various parameters x, local variables x, bound
variables x, etc. Lower <n> may require more manual allocated(x)
annotations and thus may be more difficult to use. Warning: this
option should be chosen consistently across an entire project; it
would be unsound to use different defaults for different files or
modules within a project. And even so, modes /allocated:0 and
/allocated:1 let functions depend on the allocation state, which is
not sound in general.
0 - Nowhere (never assume/assert allocated(x) by default).
1 - Assume allocated(x) only for non-ghost variables and fields
(these assumptions are free, since non-ghost variables always
contain allocated values at run-time). This option may speed up
verification relative to /allocated:2.
2 - Assert/assume allocated(x) on all variables, even bound
variables in quantifiers. This option is the easiest to use for
heapful code.
3 - (default) Frugal use of heap parameters.
4 - Mode 3 but with alloc antecedents when ranges don't imply
allocatedness.
/definiteAssignment:<n>
0 - Ignores definite-assignment rules. This mode is for testing
only--it is not sound.
1 (default) - Enforces definite-assignment rules for compiled
variables and fields whose types do not support
auto-initialization and for ghost variables and fields whose
type is possibly empty.
2 - Enforces definite-assignment for all non-yield-parameter
variables and fields, regardless of their types.
3 - Like 2, but also performs checks in the compiler that no
nondeterministic statements are used; thus, a program that
passes at this level 3 is one that the language guarantees that
values seen during execution will be the same in every run of
the program.
/noAutoReq
Ignore autoReq attributes.
/autoReqPrint:<file>
Print out requirements that were automatically generated by autoReq.
/noNLarith
Reduce Z3's knowledge of non-linear arithmetic (*,/,%).
Results in more manual work, but also produces more predictable
behavior. (This switch will perhaps be replaced by /arith in the
future. For now, it takes precedence of /arith.)
/arith:<n>
(experimental) Adjust how Dafny interprets arithmetic operations.
0 - Use Boogie/Z3 built-ins for all arithmetic operations.
1 (default) - Like 0, but introduce symbolic synonyms for *,/,%, and
allow these operators to be used in triggers.
2 - Like 1, but introduce symbolic synonyms also for +,-.
3 - Turn off non-linear arithmetic in the SMT solver. Still, use
Boogie/Z3 built-in symbols for all arithmetic operations.
4 - Like 3, but introduce symbolic synonyms for *,/,%, and allow
these operators to be used in triggers.
5 - Like 4, but introduce symbolic synonyms also for +,-.
6 - Like 5, and introduce axioms that distribute + over *.
7 - like 6, and introduce facts that associate literals arguments of *.
8 - Like 7, and introduce axiom for the connection between *,/,%.
9 - Like 8, and introduce axioms for sign of multiplication.
10 - Like 9, and introduce axioms for commutativity and
associativity of *.
/autoTriggers:<n>
0 - Do not generate {:trigger} annotations for user-level
quantifiers.
1 (default) - Add a {:trigger} to each user-level quantifier.
Existing annotations are preserved.
/rewriteFocalPredicates:<n>
0 - Don't rewrite predicates in the body of prefix lemmas.
1 (default) - In the body of prefix lemmas, rewrite any use of a
focal predicate P to P#[_k-1].
/extractCounterexample
If verification fails, report a detailed counterexample for the
first failing assertion. Requires specifying the /mv:<file> option as well
as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or
/proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and
/proverOpt:O:model.completion=true.
---- Test generation options -----------------------------------------------
/generateTestMode:<None|Block|Path>
None (default) - Has no effect.
Block - Prints block-coverage tests for the given program.
Path - Prints path-coverage tests for the given program.
Using /definiteAssignment:3 and /loopUnroll is highly recommended
when generating tests.
/warnDeadCode
Use block-coverage tests to warn about potential dead code.
/generateTestSeqLengthLimit:<n>
If /testMode is not None, using this argument adds an axiom that
sets the length of all sequences to be no greater than <n>. This is
useful in conjunction with loop unrolling.
/generateTestTargetMethod:<methodName>
If specified, only this method will be tested.
/generateTestInlineDepth:<n>
0 is the default. When used in conjunction with /testTargetMethod,
this argument specifies the depth up to which all non-tested methods
should be inlined.
---- Compilation options ---------------------------------------------------
/compileTarget:<language>
cs (default) - Compile to .NET via C#.
go - Compile to Go.
js - Compile to JavaScript.
java - Compile to Java.
py - Compile to Python.
cpp - Compile to C++.
Note that the C++ backend has various limitations (see
Docs/Compilation/Cpp.md). This includes lack of support for
BigIntegers (aka int), most higher order functions, and advanced
features like traits or co-inductive types.
/library:<value>
The contents of this file and any files it includes can be referenced from other files as if they were included.
However, these contents are skipped during code generation and verification.
This option is useful in a diamond dependency situation,
to prevent code from the bottom dependency from being generated more than once.
/optimizeErasableDatatypeWrapper:<value>
0 - Include all non-ghost datatype constructors in the compiled code
1 (default) - In the compiled target code, transform any non-extern
datatype with a single non-ghost constructor that has a single
non-ghost parameter into just that parameter. For example, the type
datatype Record = Record(x: int)
is transformed into just 'int' in the target code.
/out:<file>
Specify the filename and location for the generated target language files.
/compile:<n>
0 - Do not compile Dafny program.
1 (default) - Upon successful verification of the Dafny program,
compile it to the designated target language. (/noVerify
automatically counts as a failed verification.)
2 - Always attempt to compile Dafny program to the target language,
regardless of verification outcome.
3 - If there is a Main method and there are no verification errors
and /noVerify is not used, compiles program in memory (i.e.,
does not write an output file) and runs it.
4 - Like (3), but attempts to compile and run regardless of
verification outcome.
/Main:<name>
Specify the (fully-qualified) name of the method to use as the executable entry point.
Default is the method with the {:main} attribute, or else the method named 'Main'.
A Main method can have at most one (non-ghost) argument of type `seq<string>`
--args <arg1> <arg2> ...
When running a Dafny file through /compile:3 or /compile:4, '--args' provides
all arguments after it to the Main function, at index starting at 1.
Index 0 is used to store the executable's name if it exists.
/runAllTests:<n> (experimental)
0 (default) - Annotates compiled methods with the {:test}
attribute such that they can be tested using a testing framework
in the target language (e.g. xUnit for C#).
1 - Emits a main method in the target language that will execute
every method in the program with the {:test} attribute. Cannot
be used if the program already contains a main method. Note that
/compile:3 or 4 must be provided as well to actually execute
this main method!
/compileVerbose:<n>
0 - Don't print status of compilation to the console.
1 (default) - Print information such as files being written by the
compiler to the console.
/spillTargetCode:<n>
Explicitly writes the code in the target language to one or more files.
This is not necessary to run a Dafny program, but may be of interest when
building multi-language programs or for debugging.
0 (default) - Don't make any extra effort to write the textual
target program (but still compile it, if /compile indicates to
do so).
1 - Write the textual target program, if it is being compiled.
2 - Write the textual target program, provided it passes the
verifier (and /noVerify is NOT used), regardless of /compile
setting.
3 - Write the textual target program, regardless of verification
outcome and /compile setting.
Note, some compiler targets may (always or in some situations) write
out the textual target program as part of compilation, in which case
/spillTargetCode:0 behaves the same way as /spillTargetCode:1.
/coverage:<file>
The compiler emits branch-coverage calls and outputs into <file> a
legend that gives a description of each source-location identifier
used in the branch-coverage calls. (Use - as <file> to print to the
console.)
/optimize
Produce optimized C# code by passing the /optimize flag to csc.exe.
/optimizeResolution:<n>
0 - Resolve and translate all methods.
1 - Translate methods only in the call graph of current verification
target.
2 (default) - As in 1, but only resolve method bodies in
non-included Dafny sources.
/useRuntimeLib
Refer to a pre-built DafnyRuntime.dll in the compiled assembly
rather than including DafnyRuntime.cs verbatim.
/testContracts:<Externs|TestedExterns>
Enable run-time testing of the compilable portions of certain function
or method contracts, at their call sites. The current implementation
focuses on {:extern} code but may support other code in the future.
Externs - Check contracts on every call to a function or method marked
with the {:extern} attribute, regardless of where it occurs.
TestedExterns - Check contracts on every call to a function or method
marked with the {:extern} attribute when it occurs in a method
with the {:test} attribute, and warn if no corresponding test
exists for a given external declaration.
----------------------------------------------------------------------------
Dafny generally accepts Boogie options and passes these on to Boogie.
However, some Boogie options, like /loopUnroll, may not be sound for
Dafny or may not have the same meaning for a Dafny program as it would
for a similar Boogie program.
---- Boogie options --------------------------------------------------------
Multiple .bpl files supplied on the command line are concatenated into one
Boogie program.
/lib : Include library definitions
/proc:<p> : Only check procedures matched by pattern <p>. This option
may be specified multiple times to match multiple patterns.
The pattern <p> matches the whole procedure name and may
contain * wildcards which match any character zero or more
times.
/noProc:<p> : Do not check procedures matched by pattern <p>. Exclusions
with /noProc are applied after inclusions with /proc.
/noResolve : parse only
/noTypecheck : parse and resolve only
/print:<file> : print Boogie program after parsing it
(use - as <file> to print to console)
/pretty:<n>
0 - print each Boogie statement on one line (faster).
1 (default) - pretty-print with some line breaks.
/printWithUniqueIds : print augmented information that uniquely
identifies variables
/printUnstructured : with /print option, desugars all structured statements
/printDesugared : with /print option, desugars calls
/printLambdaLifting : with /print option, desugars lambda lifting
/freeVarLambdaLifting : Boogie's lambda lifting transforms the bodies of lambda
expressions into templates with holes. By default, holes
are maximally large subexpressions that do not contain
bound variables. This option performs a form of lambda
lifting in which holes are the lambda's free variables.
/overlookTypeErrors : skip any implementation with resolution or type
checking errors
/loopUnroll:<n>
unroll loops, following up to n back edges (and then some)
/soundLoopUnrolling
sound loop unrolling
/printModel:<n>
0 (default) - do not print Z3's error model
1 - print Z3's error model
/printModelToFile:<file>
print model to <file> instead of console
/mv:<file> Specify file to save the model with captured states
(see documentation for :captureState attribute)
/enhancedErrorMessages:<n>
0 (default) - no enhanced error messages
1 - Z3 error model enhanced error messages
/printCFG:<prefix> : print control flow graph of each implementation in
Graphviz format to files named:
<prefix>.<procedure name>.dot
/useBaseNameForFileName : When parsing use basename of file for tokens instead
of the path supplied on the command line
/emitDebugInformation:<n>
0 - do not emit debug information
1 (default) - emit the debug information :qid, :skolemid and set-info :boogie-vc-id
/normalizeNames:<n>
0 (default) - Keep Boogie program names when generating SMT commands
1 - Normalize Boogie program names when generating SMT commands.
This keeps SMT solver input, and thus output,
constant when renaming declarations in the input program.
/normalizeDeclarationOrder:<n>
0 - Keep order of top-level declarations when generating SMT commands.
1 (default) - Normalize order of top-level declarations when generating SMT commands.
This keeps SMT solver input, and thus output,
constant when reordering declarations in the input program.
---- Inference options -----------------------------------------------------
/infer:<flags>
use abstract interpretation to infer invariants
<flags> must specify exactly one of the following domains:
t = trivial bottom/top lattice
j = stronger intervals
together with any of the following options:
s = debug statistics
0..9 = number of iterations before applying a widen (default=0)
/checkInfer instrument inferred invariants as asserts to be checked by
theorem prover
/contractInfer
perform procedure contract inference
/instrumentInfer
h - instrument inferred invariants only at beginning of
loop headers (default)
e - instrument inferred invariants at beginning and end
of every block (this mode is intended for use in
debugging of abstract domains)
/printInstrumented
print Boogie program after it has been instrumented with
invariants
---- Debugging and general tracing options ---------------------------------
/trace blurt out various debug trace information
/traceTimes output timing information at certain points in the pipeline
/tracePOs output information about the number of proof obligations
(also included in the /trace output)
/break launch and break into debugger
---- Civl options ----------------------------------------------------------
/trustMoverTypes
do not verify mover type annotations on atomic action declarations
/trustNoninterference
do not perform noninterference checks
/trustRefinement
do not perform refinement checks
/trustLayersUpto:<n>
do not verify layers <n> and below
/trustLayersDownto:<n>
do not verify layers <n> and above
/trustInductiveSequentialization
do not perform inductive sequentialization checks
/civlDesugaredFile:<file>
print plain Boogie program to <file>
---- Verification-condition generation options -----------------------------
/liveVariableAnalysis:<c>
0 = do not perform live variable analysis
1 = perform live variable analysis (default)
2 = perform interprocedural live variable analysis
/noVerify skip VC generation and invocation of the theorem prover
/verifySnapshots:<n>
verify several program snapshots (named <filename>.v0.bpl
to <filename>.vN.bpl) using verification result caching:
0 - do not use any verification result caching (default)
1 - use the basic verification result caching
2 - use the more advanced verification result caching
3 - use the more advanced caching and report errors according
to the new source locations for errors and their
related locations (but not /errorTrace and CaptureState
locations)
/traceCaching:<n>
0 (default) - none
1 - for testing
2 - for benchmarking
3 - for testing, benchmarking, and debugging
/verifySeparately
verify each input program separately
/removeEmptyBlocks:<c>
0 - do not remove empty blocks during VC generation
1 - remove empty blocks (default)
/coalesceBlocks:<c>
0 = do not coalesce blocks
1 = coalesce blocks (default)
/traceverify print debug output during verification condition generation
/subsumption:<c>
apply subsumption to asserted conditions:
0 - never, 1 - not for quantifiers, 2 (default) - always
/alwaysAssumeFreeLoopInvariants
usually, a free loop invariant (or assume
statement in that position) is ignored in checking contexts
(like other free things); this option includes these free
loop invariants as assumes in both contexts
/inline:<i> use inlining strategy <i> for procedures with the :inline
attribute, see /attrHelp for details:
none
assume (default)
assert
spec
/printInlined
print the implementation after inlining calls to
procedures with the :inline attribute (works with /inline)
/recursionBound:<n>
Set the recursion bound for stratified inlining to
be n (default 500)
/smoke Soundness Smoke Test: try to stick assert false; in some
places in the BPL and see if we can still prove it
/smokeTimeout:<n>
Timeout, in seconds, for a single theorem prover
invocation during smoke test, defaults to 10.
/causalImplies
Translate Boogie's A ==> B into prover's A ==> A && B.
/typeEncoding:<m>
Encoding of types when generating VC of a polymorphic program:
p = predicates (default)
a = arguments
Boogie automatically detects monomorphic programs and enables
monomorphic VC generation, thereby overriding the above option.
/monomorphize
Try to monomorphize program. An error is reported if
monomorphization is not possible. This feature is experimental!
/useArrayTheory
Use the SMT theory of arrays (as opposed to axioms). Supported
only for monomorphic programs.
/reflectAdd In the VC, generate an auxiliary symbol, elsewhere defined
to be +, instead of +.
/prune
Turn on pruning. Pruning will remove any top-level Boogie declarations
that are not accessible by the implementation that is about to be verified.
Without pruning, due to the unstable nature of SMT solvers,
a change to any part of a Boogie program has the potential
to affect the verification of any other part of the program.
/printPruned:<file>
After pruning, print the Boogie program to the specified file.
/relaxFocus Process foci in a bottom-up fashion. This way only generates
a linear number of splits. The default way (top-down) is more
aggressive and it may create an exponential number of splits.
/randomSeed:<n>
Turn on randomization of the input that Boogie passes to the
SMT solver and turn on randomization in the SMT solver itself.
Certain Boogie inputs are unstable in the sense that changes to
the input that preserve its meaning may cause the output to change.
The /randomSeed option simulates meaning-preserving changes to
the input without requiring the user to actually make those changes.
The /randomSeed option is implemented by renaming variables and
reordering declarations in the input, and by setting
solver options that have similar effects.
/randomSeedIterations:<n>
Attempt to prove each VC n times with n random seeds. If
/randomSeed has been provided, each proof attempt will use
a new random seed derived from this original seed. If not,
it will implicitly use /randomSeed:0 to ensure a difference
between iterations.
---- Verification-condition splitting --------------------------------------
/vcsMaxCost:<f>
VC will not be split unless the cost of a VC exceeds this
number, defaults to 2000.0. This does NOT apply in the
keep-going mode after first round of splitting.
/vcsMaxSplits:<n>
Maximal number of VC generated per method. In keep
going mode only applies to the first round.
Defaults to 1.
/vcsMaxKeepGoingSplits:<n>
If set to more than 1, activates the keep
going mode, where after the first round of splitting,
VCs that timed out are split into <n> pieces and retried
until we succeed proving them, or there is only one
assertion on a single path and it timeouts (in which
case error is reported for that assertion).
Defaults to 1.
/vcsKeepGoingTimeout:<n>
Timeout in seconds for a single theorem prover
invocation in keep going mode, except for the final
single-assertion case. Defaults to 1s.
/vcsFinalAssertTimeout:<n>
Timeout in seconds for the single last
assertion in the keep going mode. Defaults to 30s.
/vcsPathJoinMult:<f>
If more than one path join at a block, by how much
multiply the number of paths in that block, to accomodate
for the fact that the prover will learn something on one
paths, before proceeding to another. Defaults to 0.8.
/vcsPathCostMult:<f1>
/vcsAssumeMult:<f2>
The cost of a block is
(<assert-cost> + <f2>*<assume-cost>) *
(1.0 + <f1>*<entering-paths>)
<f1> defaults to 1.0, <f2> defaults to 0.01.
The cost of a single assertion or assumption is
currently always 1.0.
/vcsPathSplitMult:<f>
If the best path split of a VC of cost A is into
VCs of cost B and C, then the split is applied if
A >= <f>*(B+C), otherwise assertion splitting will be
applied. Defaults to 0.5 (always do path splitting if
possible), set to more to do less path splitting
and more assertion splitting.
/vcsSplitOnEveryAssert
Splits every VC so that each assertion is isolated
into its own VC. May result in VCs without any assertions.
/vcsDumpSplits
For split #n dump split.n.dot and split.n.bpl.
Warning: Affects error reporting.
/vcsCores:<n>
Try to verify <n> VCs at once. Defaults to 1.
/vcsLoad:<f> Sets vcsCores to the machine's ProcessorCount * f,
rounded to the nearest integer (where 0.0 <= f <= 3.0),
but never to less than 1.
---- Prover options --------------------------------------------------------
/errorLimit:<num>
Limit the number of errors produced for each procedure
(default is 5, some provers may support only 1).
Set num to 0 to find as many assertion failures as possible.
/timeLimit:<num>
Limit the number of seconds spent trying to verify
each procedure
/rlimit:<num>
Limit the Z3 resource spent trying to verify each procedure
/errorTrace:<n>
0 - no Trace labels in the error output,
1 (default) - include useful Trace labels in error output,
2 - include all Trace labels in the error output
/vcBrackets:<b>
bracket odd-charactered identifier names with |'s. <b> is:
0 - no (default),
1 - yes
/proverDll:<tp>
use theorem prover <tp>, where <tp> is either the name of
a DLL containing the prover interface located in the
Boogie directory, or a full path to a DLL containing such
an interface. The default interface shipped is:
SMTLib (uses the SMTLib2 format and calls an SMT solver)
/proverOpt:KEY[=VALUE]
Provide a prover-specific option (short form /p).
/proverHelp Print prover-specific options supported by /proverOpt.
/proverLog:<file>
Log input for the theorem prover. Like filenames
supplied as arguments to other options, <file> can use the
following macros:
@TIME@ expands to the current time
@PREFIX@ expands to the concatenation of strings given
by /logPrefix options
@FILE@ expands to the last filename specified on the
command line
In addition, /proverLog can also use the macro '@PROC@',
which causes there to be one prover log file per
verification condition, and the macro then expands to the
name of the procedure that the verification condition is for.
/logPrefix:<str>
Defines the expansion of the macro '@PREFIX@', which can
be used in various filenames specified by other options.
/proverLogAppend
Append (not overwrite) the specified prover log file
/proverWarnings
0 (default) - don't print, 1 - print to stdout,
2 - print to stderr
/restartProver
Restart the prover after each query