15 Command-line reference🔗

This chapter documents every option the boogie executable accepts. The authority is the source, not the built-in help text:

• Source/ExecutionEngine/CommandLineOptionEngine.cs — the generic parser (Parse, ParseOption, ProcessInfoFlags) and the four options every Boogie-derived tool inherits.

• Source/ExecutionEngine/CommandLineParseState.cs — how an option’s argument is read (CheckBooleanFlag, GetIntArgument, GetUnsignedNumericArgument, GetDoubleArgument, ConfirmArgumentCount).

• Source/ExecutionEngine/CommandLineOptions.cs — Boogie’s own options: 97 case labels (83 of them option names, the other 14 the argument values of /printModel, /inline, /typeEncoding and /instrumentInfer) plus 55 boolean flags, and the fields they set — which carry the real defaults. Two of the boolean flags are shadowed by case labels of the same name and are unreachable, so the tool answers to 140 distinct option names in all.

• Source/BoogieDriver/BoogieDriver.cs — file-list handling and the process exit code.

This is Boogie 2 says nothing about the command line. The 2008 paper describes the language and its semantics; the tool’s option surface is not mentioned anywhere in it. Everything in this chapter comes from the implementation.

Examples in this chapter are run as boogie; the solver is Z3 5.0.0. Where an example’s output contains a // Command Line Options: banner it has been produced with /env:0 so that the banner is suppressed.

15.1 Invoking Boogie🔗

15.1.1 Usage🔗

boogie [ option ... ] [ filename ... ]

Arguments that do not begin with / or - are input files. Options and files may be interleaved freely; all files named on the command line are parsed and concatenated into a single Boogie program before resolution, unless /verifySeparately is given.

15.1.2 Option syntax🔗

An argument is treated as an option if it starts with / or -. Both prefixes are accepted for every option: /trace and -trace are the same switch. Option names are case-sensitive.

An option that takes one argument accepts it in either of two forms:

• Colon form — /print:out.bpl. The parser splits at the first colon, so the argument may itself contain colons.

• Separate form — /print out.bpl. This is not documented anywhere, but it falls out of ConfirmArgumentCount(1), which consumes args[i] when no colon argument was supplied. It works for every one-argument option.

boogie /proc Abs cli-abs.bpl

Boogie program verifier finished with 1 verified, 0 errors

The separate form is a trap for options whose argument is optional-looking. /prune takes an integer argument, so boogie /prune file.bpl tries to parse file.bpl as an integer and fails.

Boolean flags take no argument, and attaching one is an error rather than being ignored:

boogie /trace:1 cli-small.bpl

Boogie: Error: "/trace" cannot take a colon argument

Use /help for available options

Argument validation errors all take the same shape and stop the run before any file is read:

boogie /errorLimit

boogie /errorLimit cli-small.bpl

boogie /errorLimit:abc cli-small.bpl

boogie /errorLimit:-1 cli-small.bpl

Boogie: Error: "/errorLimit" expects 1 argument

Use /help for available options

Boogie: Error: Invalid argument "cli-small.bpl" to option /errorLimit

Use /help for available options

Boogie: Error: Invalid argument "abc" to option /errorLimit

Use /help for available options

Boogie: Error: Invalid argument "-1" to option /errorLimit

Use /help for available options

Note the second line: in the separate form the option swallowed the file name.

Integer arguments are read with Convert.ToInt32 and by default must be non-negative; several options add a stricter upper bound (for example /errorTrace requires 0 <= n < 3). Unsigned arguments use Convert.ToUInt32. Double arguments use Convert.ToDouble with the invariant culture and must be non-negative.

15.1.3 Unknown options behave differently on Unix🔗

CommandLineOptionEngine.Parse contains a platform test: when Path.DirectorySeparatorChar is / — that is, on Linux and macOS — an unrecognised option that begins with / is silently reclassified as a file name, on the theory that it might be an absolute path. Only the - form produces an "unknown switch" diagnostic:

boogie /notAnOption cli-abs.bpl

*** Error: '/notAnOption': Filename extension '' is not supported. Input files must be BoogiePL programs (.bpl).

boogie -notAnOption cli-abs.bpl

Boogie: Error: unknown switch: -notAnOption

Use /help for available options

Both exit with status 1. On Unix, prefer - when you want typos to be reported as typos.

15.1.4 Input files🔗

BoogieDriver.GetFileList applies two rules before anything is parsed:

• A file whose extension is .txt (case-insensitively) is read as a list of file names. Its contents are split on spaces, carriage returns and newlines, and each resulting name is added to the file list. This is undocumented. List files are not expanded recursively — a .txt named inside a .txt would be rejected in the next step.

• Every remaining name must end in .bpl. Any other extension is a fatal error.

echo 'cli-f1.bpl cli-f2.bpl' > files.txt

boogie files.txt

cli-f2.bpl(1,17): Error: this assertion could not be proved

Execution trace:

cli-f2.bpl(1,17): anon0

Boogie program verifier finished with 1 verified, 1 error

The file named stdin.bpl is special to the parser (Parser.Parse reads standard input for it), not to the driver: see Lexical structure.

15.1.5 Exit codes🔗

Boogie’s exit code is not a verification verdict. Main returns 0 unless one of a small number of conditions holds:

boogie cli-abs.bpl ; echo "exit=$?"

cli-abs.bpl(11,1): Error: a postcondition could not be proved on this return path

cli-abs.bpl(8,3): Related location: this is the postcondition that could not be proved

Execution trace:

cli-abs.bpl(10,5): anon0

Boogie program verifier finished with 1 verified, 1 error

exit=0

Scripts must therefore inspect the output text (or the /xml file), not $?. Boogie’s own test suite does exactly this: its lit tests diff the output against a .expect file.

15.2 Informational options🔗

These are handled by ProcessInfoFlags, which runs after argument parsing and before any file is read. If more than one is given, the first match in the order /version, /help, /attrHelp, /proverHelp wins, the rest are ignored, input files are not touched, and the process exits 0.

Three more options are informational in spirit:

boogie /env:2 /noVerify cli-small.bpl

---Command arguments

/env:2

/noVerify

cli-small.bpl

--------------------

Boogie program verifier finished with 0 verified, 0 errors

15.3 Selecting what to verify🔗

15.3.1 /proc and /noProc🔗

Both accumulate into lists. ExecutionEngineOptions.UserWantsToCheckRoutine decides:

• the pattern is Regex.Escaped, then every escaped * is turned back into .*, and the result is anchored with ^...$. So * is the only wildcard, and it matches any run of characters including none;

• the match is against the implementation’s verbose name — the value of {:verboseName "..."} if present, otherwise the implementation name;

• matching is case-sensitive;

• an implementation is checked when ProcsToCheck is empty or some /proc pattern matches, and no /noProc pattern matches — exclusions win.

procedure Abs(x: int) returns (r: int)

ensures 0 <= r;

{

if (x < 0) { r := -x; } else { r := x; }

}

procedure Bad(x: int) returns (r: int)

ensures 0 < r;

{

r := x;

}

boogie /proc:Abs cli-abs.bpl

Boogie program verifier finished with 1 verified, 0 errors

Case matters — *a* matches Bad but not Abs:

boogie '/proc:*a*' cli-abs.bpl

cli-abs.bpl(11,1): Error: a postcondition could not be proved on this return path

cli-abs.bpl(8,3): Related location: this is the postcondition that could not be proved

Execution trace:

cli-abs.bpl(10,5): anon0

Boogie program verifier finished with 0 verified, 1 error

boogie /noProc:Bad cli-abs.bpl

Boogie program verifier finished with 1 verified, 0 errors

Filtered-out implementations are neither verified nor inlined, but they are still parsed, resolved and type-checked, and they still contribute declarations to the program.

{:verboseName} changes both the name /proc matches and the name printed by /trace:

procedure {:verboseName "My Nice Name"} P()

{

assert true;

}

boogie /trace cli-verbosename.bpl

Parsing cli-verbosename.bpl

Coalescing blocks...

Inlining...

Verifying My Nice Name ...

[TRACE] Using prover: z3

[0.027 s, solver resource count: 98, 1 proof obligation]  verified

Boogie program verifier finished with 1 verified, 0 errors

15.3.2 /verifySeparately🔗

/verifySeparately (boolean, off by default) has an effect only when more than one file is named. Each file is then processed as its own program, from parsing through the trailer, and the overall result is the conjunction of the per-file results. Everything is reported once per file:

cli-f1.bpl and cli-f3.bpl both declare procedure A.

boogie /verifySeparately cli-f1.bpl cli-f3.bpl

Boogie program verifier finished with 1 verified, 0 errors

Boogie program verifier finished with 1 verified, 0 errors

Because the files never share a resolution scope, duplicate declarations across files stop being errors. Without the flag the same two files fail to resolve:

boogie cli-f1.bpl cli-f3.bpl

cli-f3.bpl(1,10): Error: more than one declaration of procedure name: A

1 name resolution errors detected in cli-f3.bpl

/verifySeparately also passes each file name as the program id used for result caching, so it composes with /verifySnapshots.

15.3.3 /noResolve, /noTypecheck, /noVerify🔗

All three are boolean flags, all off by default.

/noResolve and /noTypecheck return PipelineOutcome.Done from ResolveAndTypecheck, and ProcessProgram then returns without writing a trailer. The consequence is that these two options produce no output at all on success — not even the "finished with" line:

boogie /noResolve cli-small.bpl ; echo "exit=$?"

exit=0

/noVerify stops later, after Civl rewriting, inlining and dead-variable elimination, and does print a trailer:

boogie /noVerify cli-abs.bpl

Boogie program verifier finished with 0 verified, 0 errors

/noVerify is the usual companion to the printing options in Printing the program: /print runs before verification, so you rarely want to pay for the prover as well.

15.3.4 /overlookTypeErrors🔗

Boolean, off by default. It applies to resolution errors. The single site that reads OverlookBoogieTypeErrors is in Program.Resolve: if resolving a top-level declaration raised errors and that declaration is an Implementation, the errors are rolled back and the implementation is dropped. Type checking runs afterwards and is unaffected.

procedure Good()

{

assert true;

}

procedure Bad2()

{

assert undeclaredThing;

}

boogie /overlookTypeErrors cli-overlook.bpl

cli-overlook.bpl(8,9): Error: undeclared identifier: undeclaredThing

Warning: Ignoring implementation Bad2 because of translation resolution errors

Boogie program verifier finished with 1 verified, 0 errors

Replace the body with a genuine type error (assert 1 + true;) and the option makes no difference: the run still ends with 1 type checking errors detected.

15.4 Libraries🔗

/lib:name loads name.bpl as an embedded resource named Core.name.bpl from Boogie.Core.dll and appends its declarations to the program after all command-line files have been parsed. The libraries actually embedded (see Source/Core/Core.csproj) are:

The help text lists only base and node; set_size is undocumented.

boogie /lib:base cli-lib.bpl

Boogie program verifier finished with 1 verified, 0 errors

Two things surprise people:

• Dependencies are not resolved. node and set_size both use base, so loading them alone leaves every base name undeclared: boogie /lib:node cli-small.bpl reports 183 name-resolution errors and /lib:set_size reports 20, all of them inside the library itself. You must list every library you need: /lib:base /lib:node.

• A misspelled library is not fatal. It prints Error locating library: Core.nosuchlib.bpl not found, the program is abandoned, and the process still exits 0.

Libraries is a HashSet<string>, so repeating /lib:base is harmless but the order in which libraries are appended is not the order you wrote them.

Finally, ParseBoogieProgram adds base automatically whenever any top-level declaration carries a Civl attribute, and at the same time forces InferModifies on. A Civl program therefore never needs /lib:base or /inferModifies spelled out.

15.5 Printing the program🔗

15.5.1 /print and the print modifiers🔗

/print by itself emits the program immediately after parsing — before resolution, type checking, Civl rewriting or inlining. The file name - means the console, and the name may use the macros described in File-name macros and /logPrefix. Unless /env:0 is given, two comment lines precede the program:

boogie /print:- /noVerify cli-small.bpl

// Boogie program verifier version 3.5.7.0, Copyright (c) 2003-2014, Microsoft.

// Command Line Options: /print:- /noVerify cli-small.bpl

procedure Abs(x: int) returns (r: int);

ensures 0 <= r;

implementation Abs(x: int) returns (r: int)

{

if (x < 0)

{

r := -x;

}

else

{

r := x;

}

}

Boogie program verifier finished with 0 verified, 0 errors

Note that a procedure with a body is printed as a procedure declaration followed by a separate implementation, which is exactly how the parser represents it.

The modifiers change what is printed and, for three of them, when:

Because the last three add a printing point rather than moving it, the program is written out twice. So /print:out.bpl /printDesugared leaves only the second copy in out.bpl while /print:- /printDesugared shows both on the console.

/printUnstructured desugars structured statements into a goto graph while keeping the structured form in a comment:

boogie /print:- /noVerify /env:0 /printUnstructured cli-small.bpl

procedure Abs(x: int) returns (r: int);

ensures 0 <= r;

implementation Abs(x: int) returns (r: int)

{

/*** structured program:

if (x < 0)

{

r := -x;

}

else

{

r := x;

}

**** end structured program */

anon0:

goto anon3_Then, anon3_Else;

anon3_Then:

assume {:partition} x < 0;

r := -x;

return;

anon3_Else:

assume {:partition} 0 <= x;

r := x;

return;

}

Boogie program verifier finished with 0 verified, 0 errors

Internally PrintUnstructured is a three-valued field: 0 = structured only, 1 = both (what the flag sets), 2 = unstructured only. The flag can only reach 0 and 1. The only place in the source that sets 2 is the /printPassive writer, which is why the passive program printed below (/printPassive) carries no /*** structured program comment. /civlDesugaredFile and /printMeasureDesugaring set the field to 1, not 2, so their output still repeats the structured form in a comment.

/printDesugared expands calls into their assert/havoc/assume encoding, as a comment attached to the original call. Only the relevant part of the second copy is shown:

boogie /print:- /noVerify /env:0 /printDesugared cli-call.bpl

implementation Q()

{

var a: int;

call a := P(3);

/*** desugaring:

{

var call0formal#AT#x: int;

var call1old#AT#g: int;

var call2formal#AT#y: int;

call0formal#AT#x := 3;

assert 0 <= call0formal#AT#x;

call1old#AT#g := g;

havoc g, call2formal#AT#y;

assume call2formal#AT#y == call0formal#AT#x;

a := call2formal#AT#y;

}

**** end desugaring */

assert a == 3;

}

/printWithUniqueIds prefixes each identifier with the unique id of its declaration. Because /print runs before resolution, the ids are usually all NoDecl:

if (NoDecl^^x < 0)

{

NoDecl^^r := -NoDecl^^x;

}

Combine it with /printDesugared (which prints after resolution) to get real ids.

/pretty:0 turns off the line-breaking pass in TokenTextWriter. The difference only shows up when a sub-expression’s rendering exceeds 80 characters:

procedure Big(aaaaaaaaaa: int, bbbbbbbbbb: int, cccccccccc: int, dddddddddd: int)

{

assert aaaaaaaaaa < bbbbbbbbbb && bbbbbbbbbb < cccccccccc && cccccccccc < dddddddddd ==> aaaaaaaaaa < dddddddddd;

}

assert aaaaaaaaaa < bbbbbbbbbb && bbbbbbbbbb < cccccccccc && cccccccccc < dddddddddd

==> aaaaaaaaaa < dddddddddd;

versus, with /pretty:0:

assert aaaaaaaaaa < bbbbbbbbbb && bbbbbbbbbb < cccccccccc && cccccccccc < dddddddddd ==> aaaaaaaaaa < dddddddddd;

15.5.2 /printPassive🔗

/printPassive requires a file name, writes the passified program to that file directly, and is independent of /print. Because it takes an argument, giving it without one consumes the input file name (Invoking Boogie):

boogie /printPassive cli-small.bpl

*** Error: No input files were specified.

Given a file name it writes the fully passive (single-assignment, goto-only) program, at the point in VerificationConditionGenerator where passification finishes:

boogie /printPassive:passive.out cli-small.bpl > /dev/null ; cat passive.out

procedure Abs(x: int) returns (r: int);

ensures 0 <= r;

implementation Abs(x: int) returns (r: int)

{

var r#AT#0: int;

var r#AT#1: int;

anon0:

goto anon3_Then, anon3_Else;

anon3_Else:

assume {:partition} 0 <= x;

assume r#AT#1 == x;

goto GeneratedUnifiedExit;

GeneratedUnifiedExit:

assert 0 <= r#AT#1;

return;

anon3_Then:

assume {:partition} x < 0;

assume r#AT#0 == -x;

assume r#AT#1 == r#AT#0;

goto GeneratedUnifiedExit;

}

Note there is no /env banner: this writer is created directly and does not emit one. Note also that the file is rewritten from scratch every time an implementation is passified, and each write emits the whole program. The file you are left with is therefore the state of the program at the last write: with /vcsCores:1 that means every implementation appears, in passive form.

15.5.3 /printSplit, /printPruned and /printSplitDeclarations🔗

/printSplit and /printPruned share a case label and set the same field; only /printPruned is documented. Each VC split is written to prefix-name.spl, where name is the implementation name plus a suffix identifying the split, escaped for use in a file name. With - the splits go to the console (with a 100 ms sleep before each, to keep concurrent writers from interleaving).

mkdir -p sp

boogie /printSplit:sp/x cli-abs.bpl > /dev/null ; ls sp/

x-Abs--1.spl

x-Bad--1.spl

Boogie does not create the directory. If it does not exist the writer throws and the implementation is abandoned (the absolute paths have been shortened here):

boogie /printSplit:nosuchdir/x cli-abs.bpl

Advisory: Abs SKIPPED due to I/O exception: Could not find a part of the path '.../nosuchdir/x-Abs--1.spl'.

cli-abs.bpl(1,11): Verification encountered solver exception (Abs)

Advisory: Bad SKIPPED due to I/O exception: Could not find a part of the path '.../nosuchdir/x-Bad--1.spl'.

cli-abs.bpl(7,11): Verification encountered solver exception (Bad)

Boogie program verifier finished with 0 verified, 0 errors, 2 solver exceptions

The –1 suffix is "-" + SplitIndex + Token.ShortName with SplitIndex of -1; when {:focus} or {:split_here} produce manual splits the suffix becomes informative, for example Ex-2/focus[+16,-20,+25].

/printSplitDeclarations additionally appends the declarations that survived pruning for that split. It is silently ignored unless pruning is on (Split.PrintSplitDeclarations returns immediately when !Options.Prune), which makes it a convenient probe for what /prune keeps — see /prune.

15.5.4 /printInstrumented and /printInlined🔗

/printInstrumented (boolean, off) prints the program after abstract-interpretation results have been instrumented into it; it is only useful together with /infer and is described in Inference. /printInlined (boolean, off) prints each implementation after calls to {:inline} procedures have been expanded; see Inlining and loops.

15.5.5 /printCFG🔗

After resolution and type checking, writes one Graphviz file per implementation, named prefix.implName.dot. The graph is the loop-processed control flow graph, so it reflects Boogie’s view of the blocks rather than the source’s structured statements.

boogie /printCFG:cfg /noVerify cli-small.bpl > /dev/null ; cat cfg.Abs.dot

digraph G {

"anon0" [shape=box];

"anon3_Then" [shape=box];

"anon3_Else" [shape=box];

"anon0" -> "anon3_Then";

"anon0" -> "anon3_Else";

}

15.5.6 /printLean🔗

Completely undocumented. Passifies every implementation and emits the resulting verification conditions as a Lean 4 file that uses the Auto tactic library. The generated file starts with a preamble of SMT array definitions and lemmas and then one theorem per implementation. Verification still runs afterwards unless /noVerify is given. /prune is honoured: with pruning off the whole program’s declarations are emitted.

boogie /printLean:small.lean cli-small.bpl ; head -5 small.lean

Boogie program verifier finished with 1 verified, 0 errors

import Auto

import Auto.Tactic

import Auto.MathlibEmulator.Basic -- For `Real`

import Auto.Translation.SMTAttributes

open Lean Std Auto Auto.SMT.Attribute Classical

For the one-procedure program above the generated file is 146 lines: the first 97 are a fixed preamble of SMT array definitions and lemmas, then – Variables, – Functions, – Axioms and – Implementations sections, with theorem _boogie_Abs_correct at line 135.

15.5.7 /xml🔗

Writes a machine-readable transcript in parallel with the console output: one <method> element per implementation, an <assertionBatch> per VC split with the source location of each assertion, and an <error> element with the execution trace for each failure. Timings and Z3 resource counts are included.

boogie /xml:out.xml cli-abs.bpl > /dev/null ; cat out.xml

<?xml version="1.0" encoding="utf-8"?>

<boogie version="3.5.7.0" commandLine="... /xml:out.xml cli-abs.bpl">

<file name="cli-abs.bpl">

<fileFragment name="cli-abs.bpl" />

</file>

<error message="postcondition violation" file="cli-abs.bpl" line="11" column="1">

<related file="cli-abs.bpl" line="8" column="3" />

<trace>

<traceNode label="PreconditionGeneratedEntry" />

<traceNode file="cli-abs.bpl" line="10" column="5" label="anon0" />

</trace>

</error>

<method name="Abs" startTime="2026-08-07 23:09:29Z">

<assertionBatch number="0" iteration="0" startTime="2026-08-07 23:09:29Z">

<assertion file="cli-abs.bpl" line="2" column="3" />

<conclusion duration="0.0264656" outcome="valid" resourceCount="700" />

</assertionBatch>

<conclusion endTime="2026-08-07 23:09:29Z" duration="0.0264656" resourceCount="700" outcome="correct" />

</method>

<method name="Bad" startTime="2026-08-07 23:09:29Z">

<assertionBatch number="0" iteration="0" startTime="2026-08-07 23:09:29Z">

<assertion file="cli-abs.bpl" line="8" column="3" />

<conclusion duration="0.0144576" outcome="invalid" resourceCount="302" />

</assertionBatch>

<conclusion endTime="2026-08-07 23:09:29Z" duration="0.0144576" resourceCount="302" outcome="errors" />

</method>

</boogie>

(The commandLine attribute has been abbreviated above; it contains the full argument vector including the driver DLL path.)

15.5.8 File-name macros and /logPrefix🔗

Four options expand macros in their file-name argument, in CommandLineOptions.ApplyDefaultOptions — that is, after all arguments have been parsed, so the order on the command line does not matter:

The macros are applied to /xml, /print, /proverLog and /printModelToFile. /logPrefix:str appends str to the @PREFIX@ expansion, replacing / and \ with - so the result is always a single path component; it may be given more than once and the values are concatenated.

boogie /logPrefix:XY '/proverLog:log-@PREFIX@-@FILE@.smt2' cli-small.bpl > /dev/null ; ls log-*

log-XY-cli-small.bpl.smt2

15.5.9 /useBaseNameForFileName and /printVerifiedProceduresCount🔗

/useBaseNameForFileName (boolean, off) makes the parser record only the base name of each file in the tokens it produces, so diagnostics are reported against abs.bpl instead of ./some/path/abs.bpl. It also affects the file name printed in "parse errors detected in ..." messages.

/printVerifiedProceduresCount:n (0 or 1, default 1) controls whether the trailer includes the verified count:

boogie /printVerifiedProceduresCount:0 cli-abs.bpl

cli-abs.bpl(11,1): Error: a postcondition could not be proved on this return path

cli-abs.bpl(8,3): Related location: this is the postcondition that could not be proved

Execution trace:

cli-abs.bpl(10,5): anon0

Boogie program verifier finished with 1 error

15.6 Verification-condition generation🔗

15.6.1 Program transformations before VC generation🔗

The effects are visible in the passive program. With the default settings the assignments to a variable that is never read afterwards are gone:

procedure P(b: bool)

{

var y: int;

y := 1;

if (b) {

y := 2;

}

assert true;

}

boogie /liveVariableAnalysis:0 /printPassive:pb.out cli-blocks.bpl > /dev/null ; cat pb.out

procedure P(b: bool);

implementation P(b: bool)

{

var y: int;

var y#AT#0: int;

anon0:

goto anon3_Then, anon3_Else;

anon3_Else:

assume {:partition} !b;

assume y#AT#0 == 1;

goto anon2;

anon2:

assert true;

return;

anon3_Then:

assume {:partition} b;

assume y#AT#0 == 2;

goto anon2;

}

/removeEmptyBlocks:0 keeps the synthetic entry blocks. Running the same command with /removeEmptyBlocks:0 instead of /liveVariableAnalysis:0 yields a body that begins:

PreconditionGeneratedEntry:

goto 0;

0:

goto anon0;

anon0:

goto anon3_Then, anon3_Else;

/noPruneInfeasibleEdges keeps a branch whose guard is literally false reachable in the graph:

procedure P()

{

if (false) {

assert 1 == 2;

}

assert true;

}

boogie /noPruneInfeasibleEdges /printPassive:pi.out cli-infeasible.bpl > /dev/null ; cat pi.out

procedure P();

implementation P()

{

anon0:

goto anon3_Then, anon3_Else;

anon3_Else:

assume {:partition} !false;

goto anon2;

anon2:

assert true;

return;

anon3_Then:

assume {:partition} false;

assert 1 == 2;

goto anon2;

}

By default the edge from anon3_Then to anon2 is removed and anon2 is folded away.

/inferModifies rescues a program that would otherwise fail type checking:

var g: int;

procedure P()

{

g := 1;

}

boogie cli-modifies.bpl

boogie /inferModifies cli-modifies.bpl

cli-modifies.bpl(5,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g

1 type checking errors detected in cli-modifies.bpl

Boogie program verifier finished with 1 verified, 0 errors

15.6.2 /subsumption🔗

After an assertion has been turned into a proof obligation, it is normally also assumed for the rest of the path. 0 never assumes, 1 assumes except for quantified assertions, 2 always assumes. Turning subsumption off makes later assertions independent of earlier ones, at the cost of a harder VC:

procedure P(x: int)

{

assert x > 0;

assert x > -1;

}

boogie /subsumption:0 cli-subsumption.bpl

cli-subsumption.bpl(3,3): Error: this assertion could not be proved

Execution trace:

cli-subsumption.bpl(3,3): anon0

cli-subsumption.bpl(4,3): Error: this assertion could not be proved

Execution trace:

cli-subsumption.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 2 errors

boogie /subsumption:2 cli-subsumption.bpl

cli-subsumption.bpl(3,3): Error: this assertion could not be proved

Execution trace:

cli-subsumption.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 1 error

With /subsumption:1 this program behaves like /subsumption:2, since neither assertion is quantified.

The per-assertion attribute {:subsumption n} overrides the command-line setting.

15.6.3 /alwaysAssumeFreeLoopInvariants🔗

Boolean, off by default. A free invariant is always assumed at the loop head, so it is available inside the body and after the loop. What it is normally not part of is the two checking contexts that RemoveBackEdges builds: the block that enters the loop and the back-edge block. With this flag the free invariant is pushed into both (prefixOfPredicateCmdsInit and prefixOfPredicateCmdsMaintained), so two extra assumes appear in the passive program.

procedure P(n: int)

requires 0 <= n;

{

var i: int;

i := 0;

while (i < n)

free invariant 0 <= i;

{

i := i + 1;

}

assert 0 <= i;

}

boogie /printPassive:fi0.out cli-freeinv.bpl > /dev/null

boogie /alwaysAssumeFreeLoopInvariants /printPassive:fi1.out cli-freeinv.bpl > /dev/null

diff fi0.out fi1.out

14c14

<   anon0:

---

>   PreconditionGeneratedEntry:

15a16,19

>     goto anon0;

>

>   anon0:

>     assume 0 <= 0;

24a29

>     assume 0 <= i#AT#1;

assume 0 <= 0 is the invariant at the loop entry (with i still 0) and assume 0 <= i#AT#1 is the invariant at the back edge. Since a free invariant is never proved, adding it to the checking contexts can only weaken the obligations.

15.6.4 /prune🔗

CommandLineOptions.Prune is an auto-property with no initialiser, so its default is false. Pruning is off unless you ask for it.

Pruning removes top-level declarations that the implementation being verified cannot reach, using the dependency graph built from uses clauses, {:include_dep} and quantifier triggers. /printSplitDeclarations makes the difference visible, since it only prints anything when pruning is on:

function F(int): int uses {

axiom (forall x: int :: F(x) == 2 * x);

}

function G(int): int uses {

axiom (forall x: int :: G(x) == F(x) + 1);

}

procedure P(x: int)

ensures F(x) - x == x;

{ }

boogie /printSplit:- /printSplitDeclarations cli-prune.bpl

implementation P--1(x: int)

{

PreconditionGeneratedEntry:

goto anon0;

anon0:

assert F(x) - x == x;

return;

}

Boogie program verifier finished with 1 verified, 0 errors

boogie /prune:1 /printSplit:- /printSplitDeclarations cli-prune.bpl

implementation P--1(x: int)

{

PreconditionGeneratedEntry:

goto anon0;

anon0:

assert F(x) - x == x;

return;

}

function F(int) : int

uses {

axiom (forall x: int :: F(x) == 2 * x);

}

procedure P(x: int);

ensures F(x) - x == x;

implementation P(x: int)

{

assert F(x) - x == x;

}

Boogie program verifier finished with 1 verified, 0 errors

G and its axiom are gone. Two further interactions are worth knowing:

• /smoke forcibly sets Prune = false as a side effect of parsing, and does so in the option handler, so /smoke /prune:1 does enable pruning while /prune:1 /smoke does not. Order matters.

• Pruning is also what makes checker reuse conditional: CheckerPool will not reuse an idle checker across splits when Prune is on, because the axiom set differs per split.

15.6.5 Type and array encoding🔗

/typeEncoding chooses how polymorphism is compiled away. With m, Boogie first tries to monomorphise the whole program; if that fails it prints Unable to monomorphize input program: unhandled polymorphic features detected or ... : expanding type cycle detected and stops — but still exits 0, because the failure is a PipelineOutcome.FatalError raised inside ResolveAndTypecheck, and ProcessProgram treats every non-ResolvedAndTypeChecked outcome as a successful run. Note also that ResolveAndTypecheck overrides the option to Monomorphic whenever MonomorphismChecker.IsMonomorphic succeeds, so on a monomorphic program /typeEncoding:p and /typeEncoding:a have no effect. Datatypes and {:define} functions require monomorphic encoding: under p or a they are rejected with Datatypes only supported with monomorphic encoding / Functions with :define attribute only supported with monomorphic encoding.

UseArrayTheory is derived, not settable: it is !useArrayAxioms && TypeEncodingMethod == Monomorphic. So maps are compiled to the SMT theory of arrays only under monomorphic encoding, and /useArrayAxioms switches to explicit select/store axioms:

procedure P(m: [int]int, i: int, v: int)

{

assert m[i := v][i] == v;

}

boogie /proverLog:a0.smt2 cli-array.bpl

grep -nE 'Array|select|store' a0.smt2

14:(declare-fun m () (Array Int Int))

25: (=> (= (ControlFlow 0 0) 3) (let ((anon0_correct  (=> (= (ControlFlow 0 2) (- 0 1)) (= (select (store m i v) i) v))))

boogie /useArrayAxioms /proverLog:a1.smt2 cli-array.bpl

grep -nE 'Select__|Store__' a1.smt2

15:(declare-fun |Select__T@[Int]Int_| (|T@[Int]Int| Int) Int)

16:(declare-fun |Store__T@[Int]Int_| (|T@[Int]Int| Int Int) |T@[Int]Int|)

17:(assert (forall ( ( ?x0 |T@[Int]Int|) ( ?x1 Int) ( ?x2 Int)) (! (= (|Select__T@[Int]Int_| (|Store__T@[Int]Int_| ?x0 ?x1 ?x2) ?x1)  ?x2) :weight 0)))

18:(assert (forall ( ( ?x0 |T@[Int]Int|) ( ?x1 Int) ( ?y1 Int) ( ?x2 Int)) (! (=>  (not (= ?x1 ?y1)) (= (|Select__T@[Int]Int_| (|Store__T@[Int]Int_| ?x0 ?x1 ?x2) ?y1) (|Select__T@[Int]Int_| ?x0 ?y1))) :weight 0)))

30: (=> (= (ControlFlow 0 0) 3) (let ((anon0_correct  (=> (= (ControlFlow 0 2) (- 0 1)) (= (|Select__T@[Int]Int_| (|Store__T@[Int]Int_| m i v) i) v))))

/reflectAdd does nothing with the shipped back end. The only reader of ReflectAdd is VCExprASTPrinter.VisitAddOp, which is used for debug printing of VC expressions; the SMT-LIB output is produced by SMTLibLineariser, which never consults it. Comparing prover logs with and without the flag shows identical (+ a b) terms.

15.6.6 Prover-input stability🔗

/emitDebugInformation:0 suppresses the :qid and :skolemid annotations on quantifiers and the (set-info :boogie-vc-id ...) line. /normalizeNames:1 replaces Boogie names in the SMT input with $generated, $generated@@0, ... so that renaming a declaration in the source does not change the solver’s input:

boogie /proverLog:n0.smt2 cli-small.bpl

boogie /normalizeNames:1 /proverLog:n1.smt2 cli-small.bpl

sed -n '13,16p' n0.smt2 ; echo ---- ; sed -n '13,16p' n1.smt2

(declare-fun ControlFlow (Int Int) Int)

(declare-fun r@1 () Int)

(declare-fun x () Int)

(declare-fun r@0 () Int)

----

(declare-fun ControlFlow (Int Int) Int)

(declare-fun $generated () Int)

(declare-fun $generated@@0 () Int)

(declare-fun $generated@@1 () Int)

/randomizeVcIterations:n proves each VC n times with different random seeds, renaming variables and reordering declarations each time and setting matching solver options. It sets RandomSeed to 0 if /randomSeed was not given. /randomSeedIterations is a deprecated spelling of the same option, still accepted and undocumented. The per-implementation attributes {:random_seed N} override /randomSeed for one implementation.

boogie /randomizeVcIterations:3 /trace cli-small.bpl

Parsing cli-small.bpl

Coalescing blocks...

Inlining...

Verifying Abs ...

[TRACE] Using prover: z3

[0.042 s, solver resource count: 2070, 3 proof obligations]  verified

Boogie program verifier finished with 1 verified, 0 errors

The single assertion has become three proof obligations.

15.6.7 /keepQuantifier and pool instantiation🔗

Boolean, off by default. Pool-based quantifier instantiation (the {:pool} / {:add_to_pool} attributes) normally replaces a quantifier by the conjunction or disjunction of its instances. /keepQuantifier keeps the original quantifier alongside the instances. With the flag, the quantifier survives into the SMT input:

function F(int): int;

procedure P()

{

assume (forall {:pool "A"} x: int :: F(x) == x);

assert {:add_to_pool "A", 3} F(3) == 3;

}

boogie /proverLog:q0.smt2 cli-pool.bpl

boogie /keepQuantifier /proverLog:q1.smt2 cli-pool.bpl

grep -c forall q0.smt2 q1.smt2

q0.smt2:0

q1.smt2:1

15.7 Error reporting🔗

15.7.1 /errorLimit🔗

The maximum number of counterexamples extracted per verification condition. 0 means "keep going until every assertion has been falsified or proved". Note that this counts errors per VC, so splitting changes what it means.

procedure Many(a: int, b: int, c: int, d: int)

{

assert a == 1;

assert b == 2;

assert c == 3;

assert d == 4;

}

boogie cli-errs.bpl

cli-errs.bpl(3,3): Error: this assertion could not be proved

Execution trace:

cli-errs.bpl(3,3): anon0

cli-errs.bpl(4,3): Error: this assertion could not be proved

Execution trace:

cli-errs.bpl(3,3): anon0

cli-errs.bpl(5,3): Error: this assertion could not be proved

Execution trace:

cli-errs.bpl(3,3): anon0

cli-errs.bpl(6,3): Error: this assertion could not be proved

Execution trace:

cli-errs.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 4 errors

boogie /errorLimit:2 cli-errs.bpl

cli-errs.bpl(3,3): Error: this assertion could not be proved

Execution trace:

cli-errs.bpl(3,3): anon0

cli-errs.bpl(4,3): Error: this assertion could not be proved

Execution trace:

cli-errs.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 2 errors

ApplyDefaultOptions silently forces ErrorLimit = 1 when stratified inlining is active and the SMTLib back end is in use. Stratified inlining cannot be turned on from Boogie’s command line, so this only affects tools like Corral that subclass these options.

15.7.2 /errorTrace🔗

0 prints only the error line. 1 prints the labelled execution trace. 2 is documented as "include all Trace labels"; in practice the difference from 1 is rarely visible.

boogie /errorTrace:0 cli-trace.bpl

boogie /errorTrace:1 cli-trace.bpl

cli-trace.bpl(8,3): Error: this assertion could not be proved

Boogie program verifier finished with 0 verified, 1 error

cli-trace.bpl(8,3): Error: this assertion could not be proved

Execution trace:

cli-trace.bpl(3,3): anon0

cli-trace.bpl(4,7): anon4_Then

cli-trace.bpl(8,3): anon3

Boogie program verifier finished with 0 verified, 1 error

/errorTrace:0 also suppresses the counterexample model. The code that honours /printModel and /enhancedErrorMessages sits inside the if (Options.ErrorTrace > 0) branch, so /errorTrace:0 /printModel:1 prints neither trace nor model.

15.7.3 /printModel, /printModelToFile and /mv🔗

/printModel:1 prints the solver’s counterexample model after each error’s execution trace. Unlike most integer options, this one is parsed by comparing the argument string against "0" and "1", so /printModel:2 is rejected.

boogie /printModel:1 cli-trace.bpl

cli-trace.bpl(8,3): Error: this assertion could not be proved

Execution trace:

cli-trace.bpl(3,3): anon0

cli-trace.bpl(4,7): anon4_Then

cli-trace.bpl(8,3): anon3

*** MODEL

r ->

r@0 -> 1

r@1 -> 1

x -> (- 1)

ControlFlow -> {

0 0 -> 5

0 2 -> (- 1)

0 3 -> 2

0 5 -> 3

else -> 5

}

tickleBool -> {

false -> true

true -> true

else -> true

}

*** STATE <initial>

r ->

x -> (- 1)

*** END_STATE

*** END_MODEL

Boogie program verifier finished with 0 verified, 1 error

/printModelToFile:f sends the model to f instead of the console — the call site is error.Model.Write(Options.ModelWriter ?? errorInfo.Out) — so /printModel:1 /printModelToFile:f prints no model at all on standard output.

/mv:file writes the model annotated with {:captureState} points. Each assume {:captureState "s"} ... in the program becomes a *** STATE s section listing the variables whose incarnation changed:

procedure P(x: int) returns (r: int)

{

assume {:captureState "start"} true;

r := x;

assume {:captureState "afterAssign"} true;

assert r == x + 1;

}

boogie /mv:mv.out cli-capture.bpl > /dev/null ; cat mv.out

*** MODEL

r ->

x -> 0

ControlFlow -> {

0 0 -> 3

0 2 -> (- 1)

0 3 -> 2

else -> (- 1)

}

tickleBool -> {

false -> true

true -> true

else -> true

}

*** STATE <initial>

r ->

x -> 0

*** END_STATE

*** STATE start

*** END_STATE

*** STATE afterAssign

r -> 0

*** END_STATE

*** END_MODEL

/mv does not need /printModel; setting ModelViewFile is enough to make ExpectingModel true, which is what causes the solver to be asked for a model at all.

15.7.4 /enhancedErrorMessages🔗

With 1, statements carrying {:print e0, e1, ...} contribute an "augmented execution trace" showing the values of those expressions in the counterexample.

procedure P(x: int, y: int)

{

assert {:print x, y, x + y} x == y;

}

boogie /enhancedErrorMessages:1 cli-print.bpl

cli-print.bpl(3,3): Error: this assertion could not be proved

Execution trace:

cli-print.bpl(3,3): anon0

Augmented execution trace:

45x + y

Boogie program verifier finished with 0 verified, 1 error

That output is not a typo. ConditionGeneration.AddDebugInfo substitutes model values only for arguments that are plain IdentifierExprs; any other expression is printed as-is. And ExecutionEngine writes the elements with Write, with no separator. So x -> 4, y -> 5 and the literal text x + y are concatenated into 45x + y, followed by the newline the attribute handler appends.

15.7.5 /forceBplErrors🔗

Boolean, off. An assertion carrying {:msg "..."} normally reports that message instead of Boogie’s own. /forceBplErrors restores the standard message:

procedure P(x: int)

{

assert {:msg "custom message"} x == 1;

}

boogie cli-msg.bpl

boogie /forceBplErrors cli-msg.bpl

custom message

Execution trace:

cli-msg.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 1 error

cli-msg.bpl(3,3): Error: this assertion could not be proved

Execution trace:

cli-msg.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 1 error

15.7.6 /trackVerificationCoverage and /warnVacuousProofs🔗

/trackVerificationCoverage asks the solver for an unsat core and reports which program elements labelled with {:id "..."} were needed for the proof. It replaces the old undocumented /printNecessaryAssertions.

It requires /trace to print anything. Both report sites are guarded by Options.Trace:

procedure P(x: int)

requires {:id "reqPos"} 0 < x;

requires {:id "reqBig"} 100 < x;

{

assert {:id "goal"} 0 <= x;

}

boogie /trackVerificationCoverage cli-coverage.bpl

Boogie program verifier finished with 1 verified, 0 errors

boogie /trackVerificationCoverage /trace cli-coverage.bpl

Parsing cli-coverage.bpl

Coalescing blocks...

Inlining...

Verifying P ...

[TRACE] Using prover: z3

Proof dependencies:

goal

reqPos

[0.029 s, solver resource count: 547, 1 proof obligation]  verified

Proof dependencies of whole program:

goal

reqPos

Boogie program verifier finished with 1 verified, 0 errors

reqBig is absent, so it was not needed.

/warnVacuousProofs is a superset: it adds synthetic {:id} attributes to every assumption, assertion, requires, ensures and call, turns on TrackVerificationCoverage (the getter returns trackVerificationCoverage || WarnVacuousProofs), and warns when a proof goal was discharged without being covered. It reports without /trace:

procedure P(x: int)

{

assume x == 1;

assume x == 2;

assert x == 3;

}

boogie /warnVacuousProofs cli-vacuous.bpl

cli-vacuous.bpl(5,2): Warning: Proved vacuously

Boogie program verifier finished with 1 verified, 0 errors

Both options make ProduceUnsatCores true, which changes the SMT-LIB stream ((set-option :produce-unsat-cores true) and named assertions) and can therefore change solver performance.

15.7.7 /smoke and /smokeTimeout🔗

The soundness smoke test inserts assert false at various points and reports the ones the prover can discharge — those points are unreachable, which usually means an over-constrained assume or requires has silently made part of the program vacuous.

procedure P(x: int)

requires 0 < x;

{

var y: int;

if (x < 0) {

y := 1;

} else {

y := 2;

}

}

boogie /smoke cli-smoke.bpl

found unreachable code:

implementation P(x: int)

{

var y: int;

0:

goto anon0;

anon0:

goto anon3_Then;

anon3_Then:

assume {:partition} x < 0;

y := 1;

assert false;

return;

}

Boogie program verifier finished with 1 verified, 0 errors

Remember that /smoke sets Prune = false while the option is parsed.

15.8 Resource limits🔗

/timeLimit is turned into (set-option :timeout n000) per query; /rlimit into (set-option :rlimit n). The per-implementation attributes {:timeLimit N} and {:rlimit N} override them.

/processTimeLimit is described in the source as "a hidden option" and is not in the help. It cancels the top-level task after the given number of seconds. The cancellation propagates as PipelineOutcome.Cancelled, which falls through ProcessProgram’s switch to the default arm, so the run produces no output at all and exits 1:

time ( boogie /processTimeLimit:2 cli-timeout1.bpl ; echo "exit=$?" )

exit=1

real 0m2.203s

user 0m0.305s

sys 0m0.042s

(Without the limit that program runs for minutes.)

15.8.1 How a timeout is reported🔗

This is the most surprising corner of the option set. Whether a timeout looks like a timeout depends on how many assertions are in the split.

If the split contains more than one assertion, the outcome is a proper time-out:

function {:bvbuiltin "bvmul"} bvmul(bv64, bv64): bv64;

function {:bvbuiltin "bvult"} bvult(bv64, bv64): bool;

procedure Factor(x: bv64, y: bv64, k: int)

requires bvult(1bv64, x) && bvult(1bv64, y);

requires bvult(x, 4294967296bv64) && bvult(y, 4294967296bv64);

{

assert k == k;

assert bvmul(x, y) != 9223372036854775783bv64;

}

boogie /timeLimit:5 cli-timeout.bpl

cli-timeout.bpl(4,11): Verification of 'Factor' timed out after 5 seconds

Boogie program verifier finished with 0 verified, 0 errors, 1 time out

Remove the trivial first assertion and the split becomes what Split.LastChance calls a last chance — one assertion, nothing left to split. HandleProverFailure then manufactures a counterexample for it and sets the outcome to Errors:

boogie /timeLimit:5 cli-timeout1.bpl

cli-timeout1.bpl(8,3): Error: this assertion could not be proved

Execution trace:

cli-timeout1.bpl(8,3): anon0

Boogie program verifier finished with 0 verified, 1 error

A single-assertion timeout is indistinguishable from a genuine assertion failure. The same asymmetry applies to /rlimit:

boogie /rlimit:100000 cli-timeout.bpl

boogie /rlimit:100000 cli-timeout1.bpl

cli-timeout.bpl(4,11): Verification out of resource (Factor)

Boogie program verifier finished with 0 verified, 0 errors, 1 out of resource

cli-timeout1.bpl(8,3): Error: this assertion could not be proved

Execution trace:

cli-timeout1.bpl(8,3): anon0

Boogie program verifier finished with 0 verified, 1 error

15.8.2 /runDiagnosticsOnTimeout and /traceDiagnosticsOnTimeout🔗

Both are undocumented booleans, off by default. When a query times out, /runDiagnosticsOnTimeout bisects the assertions of the split, re-checking subsets with a smaller per-assertion time limit (TimeLimit / 100 * TimeLimitPerAssertionInPercent milliseconds, or 1000 ms if /timeLimit was not given), until it can name the assertions that individually time out:

boogie /runDiagnosticsOnTimeout /timeLimit:5 cli-timeout.bpl

cli-timeout.bpl(4,11): Verification of 'Factor' timed out after 5 seconds with 1 check(s) that timed out individually

cli-timeout.bpl(9,3): Unverified check due to timeout: this assertion could not be proved

Boogie program verifier finished with 0 verified, 0 errors, 1 time out

/traceDiagnosticsOnTimeout adds a report of the search itself:

boogie /runDiagnosticsOnTimeout /traceDiagnosticsOnTimeout /timeLimit:5 cli-timeout.bpl

Starting timeout diagnostics with initial time limit 5000.

Terminated timeout diagnostics after 1013 ms and 3 prover queries.

Outcome: TimeOut

Unverified assertions: 1 (of 2)

cli-timeout.bpl(4,11): Verification of 'Factor' timed out after 5 seconds with 1 check(s) that timed out individually

cli-timeout.bpl(9,3): Unverified check due to timeout: this assertion could not be proved

Boogie program verifier finished with 0 verified, 0 errors, 1 time out

The per-assertion limit here is 5000 / 100 * 10 = 500 ms, from /timeLimitPerAssertionInPercent’s default of 10.

/runDiagnosticsOnTimeout also changes cache behaviour: a cached TimedOut result is re-verified rather than reused.

15.9 Prover selection and options🔗

15.9.1 /proverDll🔗

A name without a path separator is resolved to Boogie.Provers.tp.dll next to the executing assembly; a name containing / or \ is used as a path. The DLL must export Microsoft.Boogie.tp.Factory.

In practice SMTLib is the only usable value. Boogie.Provers.LeanAuto.dll also ships, but it does not export a Factory type. Lean output is available through /printLean instead.

The option is processed eagerly, during parsing, which is why it must precede /proverHelp.

15.9.2 /proverOpt (/p)🔗

Options accumulate and are handed to the back end after parsing. An unrecognised key becomes a ProverException at verification time — and therefore exit code 1:

boogie /proverOpt:NOPE=1 cli-small.bpl ; echo "exit=$?"

Fatal Error: ProverException: Unrecognised prover option: NOPE=1

exit=1

Either = or : separates key from value, and a bare key sets the value to the empty string. The keys the shipped back end accepts (/proverHelp):