Expand description
TODO: Replace this logic by implementing a smarter interval logic
This module replaces all sums of variables by a new single variable, which is always incremented / decremented when any of its components is incremented or decremented. This replacement is sound and complete, however it is expensive, as it might generate more spurious paths.
Instead this logic should be replaced by a better ordering that can validate which intervals are possible for the sum of two variables by their individual intervals