Search code examples
z3dafny

Boogie strange assert(false) behavior

I am working with Boogie and I have come across some behaviors I do not understand.

I have been using assert(false) as a way to check if the previous assume statements are absurd.

For instance in the following case, the program is verified without errors...

type T;
const t1, t2: T;
procedure test()
{
  assume (t1 == t2);
  assume (t1 != t2);
  assert(false);
}

...as t1 == t2 && t1 != t2 is an absurd statement.

On the other hand if I have something like

type T;
var map: [T]bool;
const t1, t2: T;

procedure test()
{
  assume(forall a1: T, a2: T :: !map[a1] && map[a2]);
  //assert(!map[t1]);
  assert(false);
}

The assert(false) only fails when the commented line is uncommented. Why is the commented assert changing the result of the assert(false)?

Solution

  • Gist: the SMT solver underlying Boogie will not instantiate the quantifier if you don't mention a ground instance of map[...] in your program.

    Here is why: SMT solvers (that use e-matching) typically use syntactic heuristics to decide when to instantiate a quantifier. Consider the following quantifier:

    forall i: Int :: f(i)

    This quantifier admits infinitely many instantiations (since i ranges over an unbounded domain), trying all would thus result in non-termination. Instead, SMT solvers expect syntactic hints instructing it for which i the quantifier should be instantiated. These hints are called a patterns or triggers. In Boogie, they can be written as follows:

    forall i: Int :: {f(i)} f(i)

    This trigger instructs the SMT solver to instantiate the quantifier for each i for which f(i) is mentioned in the program (or rather, current proof search). E.g., if you assume f(5), then the quantifier will be instantiated with 5 substituted for i.

    In your example, you don't provide a pattern explicitly, so the SMT solver might pick one for you, by inspecting the quantifier body. It will most likely pick {map[a1], map[a2]} (multiple function applications are allowed, patterns must cover all quantified variables). If you uncomment the assume, the ground term map[t1] becomes available, and the SMT solver can instantiate the quantifier with a1, a2 mapped to t1, t1. Hence, the contradiction is obtained.

    See the Z3 guide for more details on patterns. More involved texts about patterns can be found, e.g. in this paper, in this paper or in this paper.