Matching Loop Detection Issues

[JonasAlaif]

A tracking issue for any logfiles for which the current ML algo fails to construct a graph.

• Log sequences-18.log. This is due to a sequence as so:

Seq_append(SIN, [⭐ → Seq_take(⭐, SUB)])
Seq_append(SIN, Seq_take([⭐ → Seq_take(⭐, SUB)], Seq_sub([⭐ → Seq_add(Seq_sub(⭐, LEN), LEN)], LEN)))
Seq_append(SIN, Seq_take(Seq_take([⭐ → Seq_take(⭐, SUB)], Seq_sub([⭐ → Seq_add(Seq_sub(⭐, LEN), LEN)], LEN)), Seq_sub(Seq_add(SUB, LEN), LEN)))
// A simplified sequence would be
g(x, y)
g(g(x, y), z)
g(g(g(x, y), z), z)

• File rewrite_at_yield.smt2 results in rewrite_at_yield.log. Or a real world example is here (from carbon):
  ListIterator.11.log. The issue is that z3 rewrites yielded terms using equalities before the yield (enode creation during instantiation) is logged, and doesn't log this rewrite in any way. Therefore the dependency on the equality is lost and the chain seems like a ML since there are no new facts coming in.