Wrong Blame Dependencies and Matched Terms

[cschmitter]

Sometimes the Axiom Profiler gives unexpected blame dependencies and incorrectly lists the matched terms for each trigger in the Selected Nodes Info section. It is not clear to me why this occurs sometimes and not others.

In the example below we have that trigger #0 matches j(i(i(i(a)))) against j(X) and that X is bound to j(i(i(i(a)))). This is the expected behavior. However trigger #1 matches i(i(i(i(a)))) against i(i(i(X))). This is incorrect. For a consistent binding of X we should expect the matched term for trigger #1 to be i(i(i(i(i(i(a)))))).

Furthermore, note that although there are only two triggers, there are four enodes blamed. i302->i303 and e432->i303 correctly indicate blame for triggers #0 and #1 (although, note that e432->i303 is incorrectly labelled #3). The other two blame dependencies list subterms of e432. I have observed this behavior, where subterms of actual matched terms are listed as dependencies in other examples as well.

Note how there are four dependencies whereas there should only be two.

This bug appears to present a bit differently in the next example, however I expect they have the same cause. Here, the matched terms listed are correct for the quantifier, however the matched terms listed for triggers #0 and #1 are swapped: it erroneously claims that cons(empty, head(b@3@01)) matches against Eq(p, q) and that Eq(e!1, empty) matches against cons(q, a).

Find attached z3 log files exhibiting this bug:
BasicSequenceAxiomatization.forupload.z3.log
CrissCross.z3.log
Disjointed.z3.log