Rework AssertionOrderModulation s.t. it uses PathPrograms instead of Trace histogram

[danieldietsch]

We want to change the assertion order whenever we unroll a loop because we did not find loop invariants in a previous iteration.

The right way to do this is to save path programs that we already have analyzed together with a counter. Whenever the counter is > 1, we change the assertion order.

The assertion order for each path program should start with non-incremental.

To aid in debugging, we also want to hash the trace we analyze and log this hash.

Taipan already constructs a cache of path programs in mKnownPathPrograms of CegarAbsIntRunner.

[Heizmann]

We would like to have a hash of trace and path program.