Don't try to make inexpressable assertions

This was producing an assertion that the return value of sparticus was
less than a number greater than it's return bitwidth could express. Z3's
response to being given this number (_ bv4 2) is to return unsat,
always. Which isn't unreasonable.

Get around this by detecting this condition and exiting early.
Nurk some tabs
Allow configuring number of slots

This allows selection of, say, 8 slots for a situation where we have two
arenas
Constrain QFBV printed vars to be in team range