Linear-size encoding of the WS axiom

Recall that the SMT-LIB 2.0 standard defines a variadic function called
"distinct" that says that variables in a list are pairwise not equal. In
addition, recall that, for all x, y in a poset P, if x != y, then x < y
or y > x. Thus, if the sort of "distinct" variables is the same total
order (e.g. Int), we conclude that their ordering is irreflexive. This
yields a linear-size encoding of the write serialization (WS) axiom.
Add Z3 benchmarks for total order encodings
Test write and read clocks separately
Add Zone and ZoneAtom copy constructor
Return reference for Zone::bottom() to avoid copying