Further adjust met-people tracking code.

Still needed to eliminate the explicit team-id part.
Calcumalate a bv of who's played who.
Declare met-goodness variables.
neva4get newlines.
Fix SMT sort failery; despair of life.

So: we have to have all operations agree on a sort. That's fine.

We also want some reasonable bit width for the team ID numbers. That's
fine too.

Finally we want to have this bitvector of who-has-played-who. That's
fine too.

The trouble is when you mix all these things, we end up having to have
all numbers having the same sort, because we're doing operations that
involve all the different kinds of numbers. And because having different
width operands to bvshl (which is something that all hardware achieves)
is apparently too difficult.

My eyes. In any case, the worse that all of this can do is cause some
inefficiency, there will never be any overflows occurring.