Question

How do I run Boogie manually? What Dafny output and command-line flags do I need?

Answer

A Boogie file is generated by Dafny using the option -print. For example, the command dafny -print:a.bpl HelloWorld.dfy will produce a file a.bpl. If the -print option lacks an argument (the file name), the somewhat confusing message Error: No input files were specified is emitted. Be cautious: dafny -print A.dfy B.dfy may overwrite A.dfy. You can also use -print:- to send the boogie file to the standard output.

To run boogie, it is most convenient to install boogie directly. See https://github.com/boogie-org/boogie. Dafny invokes Boogie as a library, not as a spawned executable, so there is no Boogie executable in the Dafny installation. However, the version of Boogie that Dafny uses corresponds to Boogie 2.15.7 (as of Dafny 3.7.3).

On a simple Hello World program, boogie a.bpl is sufficient. Dafny does rely on these default Boogie options

• smt.mbqi is set false
• model.compact is set false
• model.v2 is set true
• pp.bv_literals is set false

Dafny also sets these non-default Boogie options:

• auto_config is set false
• type_check is set true
• smt.case_split is set 3
• smt.qi.eager_threshold is set 100
• smt.delay_units is set true
• smt.arith.solver is set 2

These all however are subject to change, especially as the version of Boogie used changes

In addition, Dafny sends a variety of other command-line options to Boogie, depending on selections by the user and heuristics built-in to Dafny. Some guide to the available (Dafny) options that are passed through to Boogie are in the reference manual.