Problem using BVD with Boogie

Jan 11, 2013 at 9:33 AM

I tried to run the command :

boogie -mv:foo.model foo.bpl
the command gets executed the o/p is:
Boogie program verifier finished with 1 verified, 0 erre

but, as the foo.model file is not generated so the next command .
Please help and thanks in advance.

Jan 11, 2013 at 7:07 PM

Models are produced only for failed verifications.  In the example you show, there were 0 errors, so you don't get any models.  Try an example with an error.


Jan 12, 2013 at 7:55 AM

It is working for programs with integers,but with programs that have real variables , the model is not being generated.