Failing on nontrivial contracts with forall quantifiers

[michael-emmi]

The following array_forall example fails for a very silly reason having to do with quantifier instantiation: slight variations of the quantified expressions in the produced Boogie code — e.g., inlining an application of the identity function — result in successful verification.

#define SIZE 10
int g[SIZE];

void p() {
  ensures(forall("i", qvar("i", int) < 0 || qvar("i", int) >= SIZE || g[qvar("i", int)] == qvar("i", int)));

  for (int i=0; i<SIZE; i++) {
    invariant(forall("x", qvar("x", int) < 0 || qvar("x", int) >= i || g[qvar("x", int)] == qvar("x", int)));
    g[i] = i;
  }
}

One solution to this problem is to turn on model-based quantifier instantiation (MBQI); this can be done by passing the /z3opt:SMT.MBQI=true flag to Boogie.

It is unclear whether this is a good general-purpose solution, since this seems to slow down Boogie/Z3 quite a bit.

[zvonimir]

I am a bit confused here. I just tried to pass /z3opt:smt.mbqi=true to Boogie, and Boogie fails to prove the quantified loop invariant. What am I missing? How exactly do you invoke Boogie?

[michael-emmi]

It’s case sensitive.

[zvonimir]

Ok, when I turn on MBQI, then array_forall_fail times out. Also, what do you mean by "inlining an application of the identity function"?

[michael-emmi]

Compare the result of running Boogie on this program

const M: [int] int;
function {:inline} f(i: int) returns (int) { i }
function {:inline} g(i: int) returns (bool) { |{
  var x: int;
b:
  x := f(i);
  return M[x] > 0;
}| }
procedure p() {
  assert (forall i: int :: g(i)) ==> (forall i: int :: g(i));
}

versus this program

const M: [int] int;
function f(i: int) returns (int) { i }
function {:inline} g(i: int) returns (bool) { |{
  var x: int;
b:
  x := f(i);
  return M[x] > 0;
}| }
procedure p() {
  assert (forall i: int :: g(i)) ==> (forall i: int :: g(i));
}

where the only difference is the inlining of the identity function f. Boogie will fail when f is inlined, and succeed when it is not. When MBQI is enabled, both succeed.

[zvonimir]

Got it, thanks. Btw, do you observe the same timeout as me?

[michael-emmi]

Yes, it seems that MBQI might never terminate when the query is unsatisfiable.

[zvonimir]

I think you probably meant "when the query is satisfiable". Hmmm, ok, so what should we do with this?