Experiment with series-parallel graph slicing

Recall that v1.0 builds a series-parallel graph G of the concurrent program P
that is under scrutiny. Then, it encodes all events and their ordering in G.

In contrast, this patch encodes paths in G on an individual basis. We call
such a path in G a "slice". Observe that each slice may correspond to many
execution paths in P (with possibly many context switches). In other words,
a slice captures many concurrent executions along a chain of basic blocks
in P.

The slicing approach seems plausible when the entire partial order encoding
of G is too large for an SMT/SAT solver to efficiently handle. However, the
downside of slicing is that there could be an exponential number of slices.
In fact, the current benchmarks already expose the slowdown this causes.