Reduce legal range of identifiers for now

Even positive integers (m = 2k for k in 0 to 2^15-1) are for read
events. In turn, odd positive integers (n = 2k + 1 for k in 0 to 2^15-1)
are write events. That is, the maximal read event identifier is 2^30-2
and the maximal write event identifier is 2^30-1. These upper limits
stem from Z3 which aligns char pointers for symbol names by 4 bytes on
32-bit architectures.