@@ -833,32 +833,12 @@ module RangeStage<
833833 ) {
834834 exists ( Sem:: Expr e , D:: Delta d1 , D:: Delta d2 |
835835 unequalFlowStepIntegralSsa ( v , pos , e , d1 , reason ) and
836- boundedUpper ( e , b , d2 ) and
837- boundedLower ( e , b , d2 ) and
836+ bounded ( e , b , d2 , true , _ , _ , _ ) and
837+ bounded ( e , b , d2 , false , _ , _ , _ ) and
838838 delta = D:: fromFloat ( D:: toFloat ( d1 ) + D:: toFloat ( d2 ) )
839839 )
840840 }
841841
842- /**
843- * Holds if `b + delta` is an upper bound for `e`.
844- *
845- * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
846- */
847- pragma [ nomagic]
848- private predicate boundedUpper ( Sem:: Expr e , SemBound b , D:: Delta delta ) {
849- bounded ( e , b , delta , true , _, _, _)
850- }
851-
852- /**
853- * Holds if `b + delta` is a lower bound for `e`.
854- *
855- * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
856- */
857- pragma [ nomagic]
858- private predicate boundedLower ( Sem:: Expr e , SemBound b , D:: Delta delta ) {
859- bounded ( e , b , delta , false , _, _, _)
860- }
861-
862842 /** Weakens a delta to lie in the range `[-1..1]`. */
863843 bindingset [ delta, upper]
864844 private D:: Delta weakenDelta ( boolean upper , D:: Delta delta ) {
0 commit comments