Assert after assume doesn't verify.

Mar 15, 2011 at 4:24 PM

Why the following two assertions (after an assumption) don't verify?


#define uint unsigned int

void foo()
  uint a, b;

  assume(forall(uint j; (a == j) == (b == j)));

  assert(forall(uint j; (a == j) == (b == j)));
  assert((a == 0) == (b == 0));

Mar 15, 2011 at 4:56 PM
Edited Mar 15, 2011 at 5:06 PM

What are you actually aiming at?

Do you mean

(a == j) <==> (b == j)


Or are you trying to compare predicate definitions? I doubt VCC can do this.

Mar 15, 2011 at 7:36 PM

Well, I am just trying to understand why assertion doesn't verify. Putting <==> in place of == doesn't change anything, vcc stil can not infer it.

Another example of an assertion vcc doesn't want to prove is 

  assert(forall(uint j; j < 5; (a + j) == (b + j)) ==> a + 1 == b + 1);

And the same story if we replace + with shifting operation (e.g. comparing bytes of two integers). And that is what I need actually. But it seems like the problem is the same in all examples.

Mar 15, 2011 at 9:04 PM

These are triggering problems of Z3. An indication of that is the warning that VCC (or indeed Z3) prints here: "Prover warning: failed to find a pattern for quantifier (quantifier id: sc.11:12)". It indicates that Z3 wasn't able to select a default pattern (a.k.a. trigger) for the universally quantified assumption. Due to do that, it later has problem proving the assertion, i.e., finding the right instantiation of the assumption that would help it prove. Unfortunately, there is currently no way to deal with that automatically. Here is one way to do it manually:

#include "vcc.h"

#define uint unsigned int

void foo1()
  uint a, b;

  assume(forall(uint j; {match_ulong(j)} (a == j) == (b == j)));

  assert(forall(uint j; match_ulong(j) ==> (a == j) == (b == j)));
  // or: assert(forall(uint j; {sk_hack(match_ulong(j))} (a == j) == (b == j)));

  assert((a == 0) == (b == 0));

You can find some (potentially out-of-date) information here:

Best, Mark


Mar 15, 2011 at 9:57 PM

Thank's. This helped a lot!