Sequential loop generation: hoist the non-empty condition out of the

loop.

This allows for using a more precise implemented domain inside
the loop, eliminating the need for redundant checks when the loop is
non-empty (closes #64).

Also fixes a wraparound issue in the admissible inames finder.