Visualize the verification conditions in Dafny

Question

We are doing some academic experiments in Dafny and were wondering if there is a way to see the generated verification conditions in Dafny?

We searched the literature, websites and blogs but did not find any reference...

Answer 1

There are a few ways to do this. One way is like this:

 dafny verify --solver-option VERBOSITY=2 file.dfy

A more useful way is to generate the SMTLIB file passed into the theorem prover like this:

 dafny verify --solver-option LOG_FILE=output.smt2 file.dfy

Finally, you can also generate the intermediate Boogie file like this as well:

 dafny verify --bprint file.bpl file.dfy