Triggering problems in Z3

Question

I've recently observed several behaviours in Z3 with respect to triggering, which I don't understand. Unfortunately, the examples come from large Boogie files, so I thought I'd describe them abstractly for now, just to see if there are obvious answers. However, if the concrete files would be better, I can attach them.

There are basically three issues, although the third may well be a special case of the second. As far as my understanding goes, none of the behaviours are expected, but maybe I'm missing something. Any help would be greatly appreciated!

Firstly: Trivial equalities in my program seem to get ignored as far as triggering is concerned. For example, if t1 is a term which should match the pattern for a quantified axiom, if I add a line in my Boogie program of the form

assert t1 == t1;

then t1 does not seem to get used as a trigger for quantified axioms. I added the line explicitly in order to provide t1 as a trigger to the prover, which I often do/did in Boogie programs.

If instead I introduce an extra function, say

function f(x : same_type_as_t1) : bool
{ true }

and now instead add a line

assert f(t1);

to my program, then t1 does appear to be used as a trigger by Z3. I have checked the Z3 translation of the former program, and the (trivial) equality on t1 did survive the Boogie translation (i.e., it isn't Boogie trying to do something clever).

Secondly: Secondary patterns don't seem to be working properly for me. For example, I have a program in which one axiom has the form

axiom (forall ... :: {t1,t2} {t3,t4,t5} ..... );

and a situation in which t3, t4 and t5 have all occurred. The program fails to verify, apparently because the axiom is not instantiated. However, if I rewrite the axiom as

axiom (forall ... :: {t3,t4,t5} {t1,t2} ..... );

then the program verifies. In both cases, the time to run Boogie is approximately 3 seconds, and the patterns survive to the Z3 output.

Thirdly: This could well be a symptom of the second problem, but I was surprised by the following behaviour:

I wrote axioms of the form

axiom (forall .. :: {t1,t2} .... );

axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving t1... );

and in a situation where t2 and t3 had occurred, the first axiom didn't get instantiated (I expected it to be, since after the instantiation of the second axiom, t1 occurs). However, if I rewrote as

axiom (forall .. ::  {t2,t3} {t1,t2} .... );

axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving t1... );

then the first axiom was instantiated. However, if for some reason secondary patterns are not getting used in general, then that would also explain this behaviour.

If explicit examples would be useful, I can certainly attach long ones, and can try to cut them down a bit (but of course triggering problems are a bit delicate, so I might well lose the behaviour if I make the example too small).

Thanks a lot in advance for any advice!

Alex Summers

Edit: here is an example which partially illustrates the second and third behaviours described above. I've attached Boogie code to make it easier to read here, but I can also copy in or email the Z3 input if it'd be more useful. I've cut out almost all of the original Boogie code, but it seems hard to make it any simpler without losing the behaviour entirely.

Already the code below behaves subtly differently from my original example, but I think it's close enough. Basically the axiom labelled (1) below doesn't manage to have its second pattern set matched. If I comment out axiom (1), and instead replace it with the (currently-commented) axioms (2) and (3), which are just copies of the original with each of the two pattern sets, then the program verifies. Actually, it's enough to have axiom (2) in this particular case. In my original code (before I cut it down) it was also sufficient to flip the order of the two pattern sets in axiom (1), but that doesn't seem to be the case in my smaller repro any more.

type ref;
type HeapType;

function vals1(HeapType, ref) returns (ref);
function vals2(HeapType, ref) returns (ref);
function vals3(HeapType, ref) returns (ref);

function heap_trigger(HeapType) returns (bool);

function trigger1(ref) returns (bool);
function trigger2(ref) returns (bool);

axiom (forall Heap: HeapType, this: ref ::  {vals1(Heap, this)}  (vals1(Heap, this) == vals3(Heap,this)));

axiom (forall Heap: HeapType, this: ref :: {vals2(Heap, this)}  trigger2(this));

// (1)
axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} {trigger1(this), heap_trigger(Heap), trigger2(this)} (vals1(Heap, this) == vals2(Heap, this)));

// (2)
// axiom (forall Heap: HeapType, this: ref :: {trigger1(this), heap_trigger(Heap), trigger2(this)}  (vals1(Heap, this) == vals2(Heap, this)));
// (3)    
// axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} (vals1(Heap, this) == vals2(Heap, this)));

procedure test(Heap:HeapType, this:ref)
{
  assume trigger1(this); assume heap_trigger(Heap);

  assert (vals2(Heap, this) == vals3(Heap,this));
}

Answer 1

First question:

Trivial assertions are simplified by Z3 during a pre-processing step. The assertion assert t1 == t1 is simplified to assert true. Thus, the term t1 is not considered by the E-matching engine. The trick assert f(t1) is the standard one of making a term t1 available for E-matching for Z3. The current pre-processors in Z3 are not "smart enough" to remove the irrelevant assertion assert f(t1). Of course, a future version of Z3 may have a better pre-processor, and the trick will not work anymore.

For the second and third questions, it would be nice to have (small) Z3 scripts that produce the described behavior.

Edit. I analyzed the example in your question. It turns out this is a bug in Z3. I fixed the bug, and the fix will be available in Z3 4.1. Thanks for taking the time to reduce the size of the example. I really appreciate it. It would take “forever” to find this bug in a bigger instance. The E-matching engine was missing some instances. The problem affects Z3 scripts that contain multi-patterns that use a function symbol f that does not occur in any unary pattern. The multi-pattern should also occur before ground f-applications. Moreover, the MBQI engine must be disabled. By default, Boogie disables the MBQI engine. In this scenario, instances of the multi-pattern could be missed. This bug was in the E-matching engine for a very long time. I think it was never detected for two reasons:

1- It does not affect soundness (Z3 will not produce a wrong answer, but the “unknown” answer)

2- The MBQI engine “compensates” for any missing instance.

Regarding extra commands for providing additional terms for e-matching, we can simulate it in the following way. The command add_term(t) is just syntax sugar for (assert (add_term t)). Even if we implement a preprocessor that eliminates predicate symbols that occur only positively (or negatively), it will not eliminate the reserved predicate symbol add_term. Thus, the trick will continue to work even if we add this pre-processor.