Launch issues in Z3

Question

Recently, I noticed several behaviors in Z3 with respect to launch that I don’t understand. Unfortunately, the examples are taken from large Boogie files, so I decided to describe them abstractly at the moment, just to see if there are obvious answers. However, if specific files are better, I can attach them.

Basically there are three questions, although the third may be a special case of the second. As far as I understand, none of the behavior is expected, but maybe I missed something. Any help would be greatly appreciated!

First of all . The trivial equalities in my program seem to be ignored in relation to startup. For example, if t1 is a term that should match the template for a quantitative axiom, if I add a line to my Boogie program of the form

 assert t1 == t1; 

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

If instead I add an extra function, let's say

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

and now instead add the line

 assert f(t1); 

for my program, then t1 seems to be used as a trigger on Z3. I checked the Z3 translation of the previous program, and the (trivial) equality on t1 withstood Boogie's translation (i.e.Not Boogie is trying to do something smart).

Second: Secondary patterns do not seem to work 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 all happened. The program does not check, apparently, because the axiom is not created. However, if I rewrite the axiom as

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

then the program checks. In both cases, Boogie's startup time is approximately 3 seconds, and the patterns survive until the release of Z3.

Third: This may be a symptom of a second problem, but I was surprised by the following behavior:

I wrote axioms of form

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

and in the situation where t2 and t3 took place, the first axiom did not receive an instance (I expected this to happen, since after creating 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 created. However, if for some reason secondary patterns do not get used at all, this also explains this behavior.

If explicit examples would be useful, I can, of course, attach long ones and try to reduce them a bit (but, of course, the launch problems are a bit delicate, so I could lose my behavior if I made a small example too).

Thanks so much for any advice!

Alex Summers

Edit: Here is an example that partially illustrates the second and third behavior described above. I have attached the Boogie code to make it easier to read here, but I can also copy or email the input of Z3 if it is more useful. I cut out almost all of the original Boogie code, but it seems hard to make it simpler without losing all of the behavior.

Already the code below behaves differently compared to my original example, but I think it is close enough. Basically, the axiom labeled (1) below cannot combine its second set of patterns. If I comment on axiom (1) and replace it with axioms (2) and (3), which are only copies of the original with each of the two sets of templates, the program checks. In fact, it is enough to have axiom (2) in this particular case. In my source code (before I turned it off), it was also enough to reverse the order of the two sets of patterns in axiom (1), but this does not seem to be the case in my smaller playback.

 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 statements are simplified by Z3 during the preprocessing phase. Assertion assert t1 == t1 simplified to assert true . Thus, the term t1 not considered by the E-correspondence mechanism. The trick assert f(t1) is standard in order to make the term t1 available for E-correspondence for Z3. The current pre-processors in Z3 are not smart enough to remove the irrelevant assert f(t1) . Of course, there may be a better preprocessor in a future version of Z3, and the trick will no longer work.

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

Edit I have analyzed an 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 this. It will take "forever" to find this error in a larger instance. The E-compliance mechanism was missing in some cases. The problem affects Z3 scripts, which contain many patterns that use the function symbol f, which is not found in any inherited pattern. A multiple pattern must also be executed before ground f-applications. In addition, the MBQI engine must be turned off. By default, Boogie disables the MBQI mechanism. In this case, instances of the multi-page template may be skipped. This error has been in the E-matching engine for a very long time. I think it was not detected for two reasons:

1- This does not affect the sound (Z3 will not give an incorrect answer, but an “unknown” answer)

2- The MBQI mechanism "compensates" for any missing instance.

As for the additional teams to provide additional conditions for electronic matching, we can simulate it as follows. The add_term(t) command is just syntactic sugar for (assert (add_term t)) . Even if we implement a preprocessor that excludes predicate characters that occur only positively (or negatively), it will not eliminate the reserved predicate symbol add_term . So the trick will continue to work even if we add this pre-processor.