Options.txt

```
Use 'dafny --help' to see help for the new 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 ---------------------------------------------------------------
  
  ---- Overall reporting and printing ----------------------------------------
  
  /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.
  
  /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 --------------------------------------------
  
  /defaultFunctionOpacity:<value>
      Change the default opacity of functions. 
      `transparent` (default) means functions are transparent, can be manually made opaque and then revealed. 
      `autoRevealDependencies` makes all functions not explicitly labelled as opaque to be opaque but reveals them automatically in scopes which do not have `{:autoRevealDependencies false}`. 
      `opaque` means functions are always opaque so the opaque keyword is not needed, and functions must be revealed everywhere needed for a proof.

  /readsClausesOnMethods:<value>
      0 (default) - Reads clauses on methods are forbidden.
      1 - Reads clauses on methods are permitted (with a default of 'reads *').

  /standardLibraries:<value>
      0 (default) - Do not allow Dafny code to depend on the standard libraries included with the Dafny distribution.
      1 - Allow Dafny code to depend on the standard libraries included with the Dafny distribution.
      See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for more information.
      Not compatible with the /unicodeChar:0 option.

  /noIncludes
      Ignore include directives.
  
  /noExterns
      Ignore extern 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 - Compiled functions are written `function method` and
          `predicate method`. Ghost functions are written `function` and
          `predicate`.
      4 (default) - 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 - 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 (default) - 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.
  
  ---- 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.
  
  /warningsAsErrors
      Treat warnings as errors.
  
  ---- Verification options -------------------------------------------------
  
  /allowAxioms:<value>
      Prevents a warning from being generated for axioms, such as assume statements and functions or methods without a body, that don't have an {:axiom} attribute.

  /verificationLogger:<configuration>
      Logs verification results using the given test result format. The currently supported formats 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: --format "trx;LogFileName=<...>");
      
      The `trx` and `csv` formats automatically choose an output file name by default, and print the name of this file to the console. The `text` format prints its output to the console by default, but can send output to a file given the `LogFileName` option.
      
      The `text` format also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the isolate-assertions option, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.

  /dafnyVerify:<n>
      0 - Stop after resolution and typechecking.
      1 - Continue on to verification and compilation.
  
  /verifyAllModules
      Verify modules that come from an include directive.
  
  /emitUncompilableCode
      Allow compilers to emit uncompilable code that usually contain useful
      information about what feature is missing, rather than
      stopping on the first problem
  
  /separateModuleOutput
      Output verification results for each module separately, rather than
      aggregating them after they are all finished.
  
  /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}.
  
  /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.
      4 - Like 1, but enforces definite assignment for all local variables
          and out-parameters, regardless of their types. (Whether or not
          fields and new arrays are subject to definite assignments depends
          on their types.)
  
  /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 (experimental).
  
  ---- 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++.
      dfy - Compile to Dafny.
      
      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.
      The value may be a comma-separated list of files and folders.

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

  /runAllTests:<n>
      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!

  /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.
  
  /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:<name>    : Include definitions in library <name>. The file <name>.bpl
                   must be an included resource in Core.dll. Currently, the
                   following libraries are supported---base, node.
  /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
  /printPassive :  with /print option, prints passive version of program
  /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)
                default is -1, which means loops are not unrolled
  /extractLoops
                extract reducible loops into recursive procedures and
                inline irreducible loops using the bound supplied by /loopUnroll:<n>
  /soundLoopUnrolling
                sound loop unrolling
  /doModSetAnalysis
                automatically infer modifies clauses
  /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 ---------------------------------

  /silent       print nothing at all
  /quiet        print nothing but warnings and errors
  /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
  /trustSequentialization
                do not perform 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.
  /typeEncoding:<t>
                Encoding of types when generating VC of a polymorphic program:
                   m = monomorphic (default)
                   p = predicates
                   a = arguments
                Boogie automatically detects monomorphic programs and enables
                monomorphic VC generation, thereby overriding the above option.
                If the latter two options are used, then arrays are handled via axioms.
  /useArrayAxioms
                If monomorphic type encoding is used, arrays are handled by default with
                the SMT theory of arrays. This option allows the use of axioms instead.
  /reflectAdd   In the VC, generate an auxiliary symbol, elsewhere defined
                to be +, instead of +.
  /prune:<n>
                0 - Turn off pruning.
                1 - Turn on pruning (default). 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.

                Only use this if your program contains uses clauses
                where required, otherwise pruning will break your program.
                More information can be found here: https://github.com/boogie-org/boogie/blob/afe8eb0ffbb48d593de1ae3bf89712246444daa8/Source/ExecutionEngine/CommandLineOptions.cs#L160
  /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:<s>
                Supply the random seed for /randomizeVcIterations option.
  /randomizeVcIterations:<n>
                Turn on randomization of the input that Boogie passes to the
                SMT solver and turn on randomization in the SMT solver itself.
                Attempt to randomize and prove each VC n times using the random
                seed s provided by the option /randomSeed:<s>. If /randomSeed option
                is not provided, s is chosen to be zero.

                Certain Boogie inputs are unstable in the sense that changes to 
                the input that preserve its meaning may cause the output to change.
                This option simulates meaning-preserving changes to the input
                without requiring the user to actually make those changes.
                This option is implemented by renaming variables and reordering
                declarations in the input, and by setting solver options that have
                similar effects.
  /trackVerificationCoverage
                Track and report which program elements labeled with an
                `{:id ...}` attribute were necessary to complete verification.
                Assumptions, assertions, requires clauses, ensures clauses,
                assignments, and calls can be labeled for inclusion in this
                report. This generalizes and replaces the previous
                (undocumented) `/printNecessaryAssertions` option.

  /keepQuantifier
                If pool-based quantifier instantiation creates instances of a quantifier
                then keep the quantifier along with the instances. By default, the quantifier
                is dropped if any instances are created.

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