fix: maxVar might be larger than output var
Finally, correct model checking. Hallelujah!

Turns out the gates at k=0 needed to be in T(0,1) while it's apparently
not safe to pull the new latch states from the B partition into T(0,1).
(Although that only seemed to affect ok2.aag, while the few benchmarks
I've tested seemed fine, so maybe that's actually just a workaround /
masking another issue. We'll see if I can be bothered to investigate...)