@@ -1108,7 +1108,7 @@ module RangeStage<
1108
1108
or
1109
1109
exists ( D:: Delta dLeft , D:: Delta dRight , boolean fbeLeft , boolean fbeRight |
1110
1110
boundedSubOperandLeft ( e , upper , b , dLeft , fbeLeft , origdelta , reason ) and
1111
- boundedSubOperandRight ( e , upper , dRight , fbeRight , _ , _ ) and
1111
+ boundedSubOperandRight ( e , upper , dRight , fbeRight ) and
1112
1112
// when `upper` is `true` we have:
1113
1113
// left <= b + dLeft
1114
1114
// right >= 0 + dRight
@@ -1210,13 +1210,12 @@ module RangeStage<
1210
1210
*/
1211
1211
pragma [ nomagic]
1212
1212
private predicate boundedSubOperandRight (
1213
- SemSubExpr sub , boolean upper , D:: Delta delta , boolean fromBackEdge , D:: Delta origdelta ,
1214
- SemReason reason
1213
+ SemSubExpr sub , boolean upper , D:: Delta delta , boolean fromBackEdge
1215
1214
) {
1216
1215
// `semValueFlowStep` already handles the case where one of the operands is a constant.
1217
1216
not semValueFlowStep ( sub , _, _) and
1218
- bounded ( sub .getRightOperand ( ) , any ( SemZeroBound zb ) , delta , upper .booleanNot ( ) , fromBackEdge ,
1219
- origdelta , reason )
1217
+ bounded ( sub .getRightOperand ( ) , any ( SemZeroBound zb ) , delta , upper .booleanNot ( ) , fromBackEdge , _ ,
1218
+ _ )
1220
1219
}
1221
1220
1222
1221
pragma [ nomagic]
0 commit comments