Here is the plan

1. In quantified expressions, contracts: no functions and arguments to % and / should be non-negative (otherwise it will be an undefined behavior);
2. IntDivTransformer will skip quantifiers, contracts; (no need for transformation)
3. work on static analysis for intervals
4. repeal (1) and (2)