What version of Z3?

Apr 18, 2011 at 12:41 AM

When verifying the following code, I am getting different answers with different versions of Z3, which really puzzles me.

public class Program {
  static void Main(string![]! args)
    ensures false;
  {
    Console.WriteLine("Spec# says hello!");
  }
}

I am expecting to get an error about an unsatisfied postcondition. With Z3 versions 2.9, 2.13, 2.15, and 2.16 I get "unsatisfied postcondition: false", as expected.

With Z3 version 2.17 and 2.18, I get "verification inconclusive", which is a bit unsatisfactory.

With Z3 version 2.19, I get no error at all, so this verifier seems to think 'false' can be a correct postcondition?

I am using the 2011-04-17 nightly build of sscboogie, registered in VS 2010. Each time I install a new version of Z3, I first remove all others. I have set RunProgramVerifier and RunProgramVerifierWhileEditing to true. I also get an error with no version of Z3 installed, as expected.

What is the right version of Z3 to use with Spec#? Any hint would be appreciated ...

Coordinator
Apr 18, 2011 at 1:57 AM

See http://boogie.codeplex.com/discussions/251963.  Use Z3 version 2.15.