Optimize encodings of coherence and acyclicity (mostly IDL)

[ThomasHaas]

This PR adds a little trick to make the ordering constraints of some must-edges unconditional, i.e., it changes the encoding from exec(x) /\ exec(y) => clk(x) < clk(y) to clk(x) < clk(y) if possible.
The argument for when this can be done is quite subtle.

Most benefit is expected on eager encodings, especially for SC where I saw improvements in the range of 10-30%.
I think it might be worth having an SVCOMP run with this branch.

The optimization might also be applicable to the SAT encodings for acyclicty. I have not thought about this yet though.

EDIT: I have added the same optimization to the SAT encoding for acyclicity. I also saw some improvement, but not as big as in the IDL case.

[ThomasHaas]

See cna.c in #1016 for a benchmark where the optimizations of this PR are quite effectful.
IIRC, this is particularly the case for verifying program_spec of the #define FAIL version, where solving time went from 16 minutes down to 4-5 (using Z3/IDL encoding).