How about hard-coding goodness constraints?

Also ineffective...
Try using Z3's enum datatype for a bit.

Basically, this makes an enum instead of a BV of values. All we really
care about anyway is that the slot positions are distinct, their numeric
value is meaningless.

Leads to at least 10x speedup. Downside: we have to use Z3. Deal with
it.
Mention using Int's hasn't benefited performance.

At least 6x slower, benchmark hasn't completed yet, it probably takes
longer (also: is officially undecideable)
Use a bv bitwidth of 4.

We're not expecting to have 15 or more:
 * rounds
 * matches-per-round
 * teams-per-match

At this point in time (might change in the future). The result of this
change is a 9x speedup in performance.
Shorten slot domain to 2 bits.

Basically, it's always going to be 4-corners for the forseeable future
(ahem), so avoid some needless constraints by building some of our
validity checks into the type system.