@@ -1549,7 +1549,8 @@ private float getGuardedUpperBound(VariableAccess guardedAccess) {
     // that there is one predecessor, albeit somewhat conservative.
     exists(unique(BasicBlock b | b = def.(BasicBlock).getAPredecessor())) and
     guardedAccess = def.getAUse(v) and
-    result = max(float ub | upperBoundFromGuard(guard, guardVa, ub, branch))
+    result = max(float ub | upperBoundFromGuard(guard, guardVa, ub, branch)) and
+    not convertedExprMightOverflow(guard.getAChild+())
   )
 }
 
 
@@ -599,6 +599,10 @@
 | test.c:675:7:675:7 | y | -2147483648 |
 | test.c:684:7:684:7 | x | -2147483648 |
 | test.c:689:7:689:7 | x | -2147483648 |
+| test.c:696:8:696:8 | x | 2147483647 |
+| test.c:696:12:696:12 | y | 256 |
+| test.c:697:9:697:9 | x | 2147483647 |
+| test.c:698:9:698:9 | y | 256 |
 | test.cpp:10:7:10:7 | b | -2147483648 |
 | test.cpp:11:5:11:5 | x | -2147483648 |
 | test.cpp:13:10:13:10 | x | -2147483648 |
 
@@ -689,3 +689,12 @@ void test(int x) {
   out(x);
   goto label;
 }
+
+void test_overflow() {
+  const int x = 2147483647; // 2^31-1
+  const int y = 256;
+  if ((x + y) <= 512) {
+    out(x);
+    out(y);
+  }
+}
@@ -599,6 +599,10 @@
 | test.c:675:7:675:7 | y | 2147483647 |
 | test.c:684:7:684:7 | x | 2147483647 |
 | test.c:689:7:689:7 | x | 15 |
+| test.c:696:8:696:8 | x | 2147483647 |
+| test.c:696:12:696:12 | y | 256 |
+| test.c:697:9:697:9 | x | 2147483647 |
+| test.c:698:9:698:9 | y | 256 |
 | test.cpp:10:7:10:7 | b | 2147483647 |
 | test.cpp:11:5:11:5 | x | 2147483647 |
 | test.cpp:13:10:13:10 | x | 2147483647 |
Original file line number	Diff line number	Diff line change
`@@ -1549,7 +1549,8 @@ private float getGuardedUpperBound(VariableAccess guardedAccess) {`
`1549`	`1549`	`// that there is one predecessor, albeit somewhat conservative.`
`1550`	`1550`	`exists(unique(BasicBlock b \| b = def.(BasicBlock).getAPredecessor())) and`
`1551`	`1551`	`guardedAccess = def.getAUse(v) and`
`1552`		`- result = max(float ub \| upperBoundFromGuard(guard, guardVa, ub, branch))`
	`1552`	`+ result = max(float ub \| upperBoundFromGuard(guard, guardVa, ub, branch)) and`
	`1553`	`+ not convertedExprMightOverflow(guard.getAChild+())`
`1553`	`1554`	`)`
`1554`	`1555`	`}`
`1555`	`1556`