Skip to content

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

Matt Wala requested to merge loop-nonempty-checks into master

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.

Merge request reports