Every thread has at least one event with no predecessors
Detect deadlocks when matchable set is empty

In communication init axiom, define "\/ \emptyset" to be satisfiable.
Avoid UnsafeTerm to Bool conversion in communication concurrency axiom

The current return type of smt::implies(UnsafeTerm, Bool) is UnsafeTerm.
Then, the conversion from UnsafeTerm to Bool calls UnsafeTerm::Bool().
But this currently requires pointer casts that can fail even when
UnsafeTerm::sort().is_bool(). To be fixed later.
Tracer::flip() resets thread identifiers
Encode value semantics of Channel<T>

The extension axiom now requires the guards of matching sends and
receives to be true. In addition, every matching pair of send and
receive event implies that their terms are equal. This new feature
permits us to detect communication deadlocks even when the control-
flow in the program under scrutiny depends on sends/receives.