Z3 - getting started. Z3 seems to ignore my constraints

Reply

ElenaPavlova Posted: 05-19-2009 4:07 AM

rated by 0 users

Greetings,

I was expirementing with Z3 in Visual Studio 2008 IDE.

here is a simple C# code with an ensures constraint

public class testClass

{

public int testMethod ()

ensures 3>4;

{ return 2;}

}

As far as I understood, IDE Build command should try to verify and compile this code and issue warnings or errors -

because the constraint never holds. Unfortunately it didn't show any. I suppose Z3 was installed successfully and is working for it shows "reciever might be null warnings" for the Bag class given in examples and articles.

Where am I wrong? may be z3 was installed incorrectly? may be I try to use Z3 for things it isn't intended for?

Thank you

P.S. Probably this should be in the spec# forum, sorry

Reply

Nikolaj Bjorner replied on 06-12-2009 12:01 PM

rated by 0 users

The issue seems to be related to your Spec# installation. Spec# is responsible for generating the verification conditions and then producing formulas related to these. Indeed the ensures statement should never hold.

Thanks

Nikolaj