@@ -833,32 +833,12 @@ module RangeStage<
833
833
) {
834
834
exists ( Sem:: Expr e , D:: Delta d1 , D:: Delta d2 |
835
835
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
838
838
delta = D:: fromFloat ( D:: toFloat ( d1 ) + D:: toFloat ( d2 ) )
839
839
)
840
840
}
841
841
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
-
862
842
/** Weakens a delta to lie in the range `[-1..1]`. */
863
843
bindingset [ delta, upper]
864
844
private D:: Delta weakenDelta ( boolean upper , D:: Delta delta ) {
0 commit comments