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".

[blishko]

Similar situation in benchmark chc-LIA-Lin_486.smt2.
We should implement Z3's inline_linear preprocessing.
The idea is to check, for an outgoing linear clause, if it can be unified with exactly one (or at most one?) incoming clause to the first clause' source.
If that is the case, we can remove this outgoing edge and add a direct edge to the successor.
We could go with some cheap unification check, e.g., if we know the state variables must be constants.