Fixed performance, broke correctness when splitting SFs.

But broke correctness: Suppose k = 1. When we split an SF literal,
we have k = 0 afterwards and thus cannot do any other split.
This other split could occur in another iteration, but then the SF
cannot be split because then k = 0.

Maybe we shouldn't decrement k when we split an SF.