CODEWITHSUNDEEP
dafnyformal-verification
Costel Anghel
Costel Anghel

Reputation: 1

Visualize the verification conditions in Dafny

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

Upvotes: 0

Views: 136

Answers (1)

redjamjar
redjamjar

Reputation: 771

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

Upvotes: 0

Related Questions