Generating the Z3 model from Boogie file

Oct 28, 2014 at 3:08 PM

Is it possible to generate the Z3 file from Boogie. I've looked at the options and tried the following:
Boogie.exe /printModelToFile:simple.z3 simple.bpl
I get the following message:
Boogie program verifier version 2.2.30705.1126, Copyright (c) 2003-2014, Microsoft.

Boogie program verifier finished with 1 verified, 0 errors
But I do not get the z3 file.

Any idea? Thanks.
Oct 28, 2014 at 3:59 PM
I presume you want SMTLIB query that is passed to Z3? If that is the case the can use the /proverLog:<file> option. E.g.
$ boogie /proveLog:foo.smt2 foo.bpl
Marked as answer by tsans on 10/28/2014 at 9:50 AM
Oct 28, 2014 at 4:53 PM
Perfect. Thanks.

Small typo, it's "proverLog":
$ boogie /proverLog:foo.smt2 foo.bpl