Localisation of non-quantifier dependencies

[kiranandcode]

Is there some way to identify dependencies on non-quantifier terms in a z3 file?

To clarify what I mean, I have this simple SMT Query (in boogie form for simplicity):

axiom (forall x y z :: {length(x), length(y), empty(z)}
                          (non_empty(x) || non_empty(y)) == non_empty(append(x,y)));

axiom (forall x :: {non_empty(x)} non_empty(x) == (1 <= length(x)));

axiom (empty(null));

procedure foo(x : Seq, y : Seq)
     requires non_empty(x);
     requires non_empty(y); 
     ensures non_empty(append(x,y)); {
}

So the point is that the key axiom (the first one) has a trigger that can only be activated by a term that is produced by two irrelevant axioms -- the second axiom and the third axiom.

By using the axiom-profiler, I can identify that the second axiom is used and which part of the source file is used (by the qid), but I don't know how to recover the location of the third axiom because it is not a quantified expression:

This is the resulting graph on the online gui:

the enode e11 is corresponds to the term that was needed to prove unsat, but there is no metadata associated with it that would allow me to infer which line in the source it corresponds to.

Is this information recoverable from the smt log file?