SF literals are not split anymore.

Important: the recursion then needs to stop when k <= 0.
Before, it was k < 0.

A better way to introduce splitting of SF literals that don't count
towards the k-limit would be to use clause_sf() when k == 0 is reached.

For some reason, the unit test test_morri_example() takes very long and
fails due to timeout. The unit test test_morri_example_with_context()
still works. This issue only occurs when setup_clause_small_pel() uses
clause_pel() which also adds SF literals. It is independent of
consistency checks.