how to use z3 v2 compiler?

Jun 22, 2010 at 1:01 PM

Hello,

I am trying to use specsharp with the z3 v2 verifier.

I am unsure exactly what steps I am supposed to take in order to implement it.

I have simply put the z3.exe file in the lastknowngood9 directory.

Now, this works with z3 v1 but with z3 v2 I get yellow font errors: 'Mc.[a name] SKIPPED because of internal error: unexpected prover output : Expected ": ", found: ' &

                                                                                               'Error setting 'PARTIAL_MODELS', reason: unknown parameter'

 

I got these errors when I installed the binaries. I also tried the source code and I have exactly the same problem.

Do you think you might be able to tell me exactly what steps I should take to get the z3 v2 verifier working?

Thanks!

Jul 15, 2010 at 6:18 PM

Dear Simon

 

I am new to SpecSharp and face exactly the same problems as you describe above: the yellow error messages.

 

In addition, I can't see SpecSharp projects in Visual Studio.  However, I have installed Visual Studio 2010, not 2008.

 

I would be glad if you could provide some help, in the case you have already solved those problems.

 

Many thanks in advance

 

Edgar

 

Jul 15, 2010 at 10:40 PM

Hi Edgar,

I have not solved the problems, but I understand it is only a contingent problem that will be resolved in due course.

The z3.1 tool works, and can handle most situations, all or most of the class commands (object invariants, [Additive], expose, [Rep], [Peer] etc.).

There are issues using the product comprehension, and often multiplying two variables in e.g. an invariant.

However, the Simplify verifier seems to handle many, but not all, of these issues, as the tools stand.

There are instructions about installing Simplify here:

http://people.cs.kuleuven.be/~bart.jacobs/specleuven/

You can use it like this: sscboogie file.exe /prover:Simplify

Also, you can append /simplifyMatchDepth:5, or another integer, and this will sometimes encourage the prover enough to return a positive.

However z3.1 still works best in most circumstances.

I also use Visual Studio 2010 at home, and cannot use the as-you-code Visual Studio 2008 features.

However I find the VS command line works well - I just save textfiles from VS as .ssc.

Hope some of that helps,

Simon

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Coordinator
Jul 17, 2010 at 12:20 AM

Please see my answer today to Discussion issue "Unable to start the process z3.exe from default location".  We're working on a new binary release that will install correctly (if you're willing to build everything from source, it seems to work).

Jul 17, 2010 at 4:22 PM

Many thanks to Simon for your big help (Z3 version 1.2 as well as Simplify seem to work) and to Rustan for your detailed explanations.

Edgar

 

Coordinator
Jul 21, 2010 at 5:40 AM

Edgar and Simon,

Thanks for your patience.  We just cut a new binary release, which I hope will solve these problems.  Please see the updated installation instructions "How to install the binaries".  While you can use command-line switches with the program verifier to ask it to use Simplify or Z3 version 1.x, I recommend you install the latest Z3 (which is version 2.9), which this new Spec# release will find in the place where Z3 wants to install itself.

Let me know of further problems.

  Rustan