Is there some way to run Z3 over hand-made verification conditions?

Oct 30, 2013 at 12:04 PM
I'm preparing an undergraduate course on "Formal Methods for Software Development". I would like to show the students a little of how Dafny works. To this end, I would like to run Z3 over handmade verification conditions to show the Z3-answer. Is there some way to do that?
Oct 30, 2013 at 1:28 PM

sure, Z3 accepts input in the SMT-LIB format (see for some examples and for a tutorial). You could also check out the /proverLog command line option in Dafny to see what the VCs look like that Dafny/Boogie produce.

Best regards,

Oct 30, 2013 at 2:39 PM
Hi Valentin,

Could you tell me where could I find information about "the /proverLog command line option".
I use Dafny on Visual Studio, migth I see the VCs from there?

Oct 31, 2013 at 2:16 PM
Hi Paqui,

you can find out a bit more about the option using Dafny's /help command line option, but usually all you need to do is add /proverLog:log.smt2 to your normal Dafny invocation. The file 'log.smt2' will then contain all the VCs.

Currently, there is no way to produce this log from within Visual Studio.

Best regards,

Oct 31, 2013 at 2:42 PM

Thanks again,