BMC engine is slow compared to Z3

[blishko]

On the following benchmark, Golem is much slower than Z3: chc22/LIA-lin/chc-LIA-Lin_442.smt2
It looks like Z3 can successfully simplify the system in preprocessing.
We should try to do something similar.

[blishko]

Looks like Z3 is doing some interesting preprocessing where it detects that a recursive clause cannot be taken more than once (because its tail does not unify with its head).
Z3 can then resolve this clause and delete it completely, effectively removing one cycle from the graph.
We could do something similar, check all the cycles and if we detect that the recursive clause cannot be taken, we can (in the graph terminology) split the vertex into "in" and "out" version, and change the self loop edge into a bridge from "in" to "out".