diff --git a/java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/DfaMemoryStateImpl.java b/java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/DfaMemoryStateImpl.java
index 4505f857357a..a3c78a10219e 100644
--- a/java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/DfaMemoryStateImpl.java
+++ b/java/java-analysis-impl/src/com/intellij/codeInspection/dataFlow/DfaMemoryStateImpl.java
@@ -718,9 +718,6 @@ public class DfaMemoryStateImpl implements DfaMemoryState {
       }
       DfaVariableValue left = sum.getLeft();
       DfaValue right = sum.getRight();
-      if (appliedRange.equals(LongRangeSet.point(0)) && sum.isNegation()) {
-        return applyCondition(myFactory.createCondition(left, RelationType.EQ, right));
-      }
       LongRangeSet leftRange = getValueFact(left, DfaFactType.RANGE);
       LongRangeSet rightRange = getValueFact(right, DfaFactType.RANGE);
       if (leftRange == null || rightRange == null) return true;
@@ -886,7 +883,8 @@ public class DfaMemoryStateImpl implements DfaMemoryState {
   }
 
   private boolean applySumRelations(DfaValue left, RelationType type, DfaValue right) {
-    if (left instanceof DfaSumValue && right instanceof DfaVariableValue) {
+    if (type != RelationType.LT && type != RelationType.GT && type != RelationType.NE && type != RelationType.EQ) return true;
+    if (left instanceof DfaSumValue) {
       DfaSumValue sum = (DfaSumValue)left;
       LongRangeSet leftRange = getValueFact(sum.getLeft(), DfaFactType.RANGE);
       LongRangeSet rightRange = getValueFact(sum.getRight(), DfaFactType.RANGE);
@@ -895,51 +893,71 @@ public class DfaMemoryStateImpl implements DfaMemoryState {
       LongRangeSet rightNegated = rightRange.negate(isLong);
       LongRangeSet rightCorrected = sum.isNegation() ? rightNegated : rightRange;
 
-      if (!sum.isNegation()) {
-        RelationType correctedType = type;
-        if (type == RelationType.LT || type == RelationType.GT) {
-          boolean overflowPossible = true;
-          if (!isLong) {
-            LongRangeSet other = getValueFact(right, DfaFactType.RANGE);
-            LongRangeSet overflowRange = getIntegerSumOverflowValues(leftRange, rightCorrected);
-            overflowPossible = other == null || other.intersects(overflowRange);
+      LongRangeSet resultRange = getValueFact(right, DfaFactType.RANGE);
+      RelationType correctedRelation = correctRelation(type, leftRange, rightCorrected, resultRange, isLong);
+      if (sum.isNegation()) {
+        if (resultRange != null) {
+          long min = resultRange.min();
+          long max = resultRange.max();
+          if (min == 0 && max == 0) {
+            // a-b (rel) 0 => a (rel) b
+            if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedRelation, sum.getRight()))) return false;
           }
-          if (overflowPossible) {
-            correctedType = RelationType.NE;
+          else if (min >= 0 && RelationType.GE.isSubRelation(type)) {
+            RelationType correctedGt = correctRelation(RelationType.GT, leftRange, rightCorrected, resultRange, isLong);
+            if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedGt, sum.getRight()))) return false;
+          }
+          else if (max <= 0 && RelationType.LE.isSubRelation(type)) {
+            RelationType correctedLt = correctRelation(RelationType.LT, leftRange, rightCorrected, resultRange, isLong);
+            if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedLt, sum.getRight()))) return false;
+          }
+          if (RelationType.EQ.equals(type) && !resultRange.contains(0)) {
+            // a-b == non-zero => a != b
+            if (!applyRelation(sum.getLeft(), sum.getRight(), true)) return false;
           }
         }
+      }
+      if (right instanceof DfaVariableValue) {
         // a+b (rel) c && a == c => b (rel) 0 
         if (areEqual(sum.getLeft(), right)) {
-          if (!applyCondition(myFactory.createCondition(sum.getRight(), correctedType, myFactory.getInt(0)))) {
-            return false;
-          }
+          RelationType finalRelation = sum.isNegation() ? correctedRelation.getFlipped() : correctedRelation;
+          if (!applyCondition(myFactory.createCondition(sum.getRight(), finalRelation, myFactory.getInt(0)))) return false;
         }
         // a+b (rel) c && b == c => a (rel) 0 
-        if (areEqual(sum.getRight(), right)) {
-          if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedType, myFactory.getInt(0)))) {
-            return false;
+        if (!sum.isNegation() && areEqual(sum.getRight(), right)) {
+          if (!applyCondition(myFactory.createCondition(sum.getLeft(), correctedRelation, myFactory.getInt(0)))) return false;
+        }
+
+        if (!leftRange.subtractionMayOverflow(sum.isNegation() ? rightRange : rightNegated, isLong)) {
+          // a-positiveNumber >= b => a > b
+          if (rightCorrected.max() < 0 && RelationType.GE.isSubRelation(type)) {
+            if (!applyLessThanRelation(right, sum.getLeft())) return false;
+          }
+          // a+positiveNumber >= b => a > b
+          if (rightCorrected.min() > 0 && RelationType.LE.isSubRelation(type)) {
+            if (!applyLessThanRelation(sum.getLeft(), right)) return false;
           }
         }
-      }
-
-      if (!leftRange.subtractionMayOverflow(sum.isNegation() ? rightRange : rightNegated, isLong)) {
-        // a-positiveNumber >= b => a > b
-        if (rightCorrected.max() < 0 && RelationType.GE.isSubRelation(type)) {
-          if (!applyLessThanRelation(right, sum.getLeft())) return false;
+        if (RelationType.EQ == type && !rightRange.contains(0)) {
+          // a+nonZero == b => a != b
+          if (!applyRelation(sum.getLeft(), right, true)) return false;
         }
-        // a+positiveNumber >= b => a > b
-        if (rightCorrected.min() > 0 && RelationType.LE.isSubRelation(type)) {
-          if (!applyLessThanRelation(sum.getLeft(), right)) return false;
-        }
-      }
-      if (RelationType.EQ == type && !rightRange.contains(0)) {
-        // a+nonZero == b => a != b
-        if (!applyRelation(sum.getLeft(), right, true)) return false;
       }
     }
     return true;
   }
 
+  private static RelationType correctRelation(RelationType relation, LongRangeSet summand1, LongRangeSet summand2,
+                                              LongRangeSet resultRange, boolean isLong) {
+    if (relation != RelationType.LT && relation != RelationType.GT) return relation;
+    boolean overflowPossible = true;
+    if (!isLong) {
+      LongRangeSet overflowRange = getIntegerSumOverflowValues(summand1, summand2);
+      overflowPossible = !overflowRange.isEmpty() && (resultRange == null || resultRange.fromRelation(relation).intersects(overflowRange));
+    }
+    return overflowPossible ? RelationType.NE : relation;
+  }
+
   @NotNull
   private static LongRangeSet getIntegerSumOverflowValues(LongRangeSet left, LongRangeSet right) {
     if (left.isEmpty() || right.isEmpty()) return LongRangeSet.empty();
diff --git a/java/java-tests/testData/inspection/dataFlow/fixture/Algebraic.java b/java/java-tests/testData/inspection/dataFlow/fixture/Algebraic.java
index 9ad87d9b78bb..ad719c56cb64 100644
--- a/java/java-tests/testData/inspection/dataFlow/fixture/Algebraic.java
+++ b/java/java-tests/testData/inspection/dataFlow/fixture/Algebraic.java
@@ -1,6 +1,18 @@
 import java.util.*;
 
 public class Algebraic {
+  void testOverflowDetection(int[] arr1, int[] arr2, int offset) {
+    int l1 = arr1.length;
+    int l2 = arr2.length;
+    if (l1 < l2 || offset < 0) return;
+    if (l1 - offset >= l2) {
+      if (l1 == l2 && <warning descr="Condition 'offset == 0' is always 'true' when reached">offset == 0</warning>) {}
+    }
+    if (l1 - offset <= l2) {
+      if (l1 == l2 && offset == 0) {}
+    }
+  }
+
   void test(int x, int y) {
     if (x + 1 > 0) {
       if (<warning descr="Condition 'x == -2' is always 'false'">x == -2</warning>) {
@@ -39,7 +51,10 @@ public class Algebraic {
         || startOffset + length < 0) {
       throw new IndexOutOfBoundsException();
     }
-    if (<warning descr="Condition 'startOffset == buffer.length && length > 0' is always 'false'">startOffset == buffer.length && <warning descr="Condition 'length > 0' is always 'false' when reached">length > 0</warning></warning>) {
+    // This is always false, but we cannot reliably detect this yet. If startOffset == buffer.length
+    // then startOffset + length <= buffer.length implies that length == 0 *or* startOffset + length overflows
+    // The latest case is ruled out by startOffset + length < 0, but our memory state is unable to track this. 
+    if (startOffset == buffer.length && length > 0) {
     }
   }
 
@@ -78,4 +93,26 @@ public class Algebraic {
     if (c < 1 || c > text.length() - 1) return;
     if (<warning descr="Condition 'text.length() > c' is always 'true'">text.length() > c</warning>) {}
   }
+
+  void testDiff(int x, int y) {
+    if (<warning descr="Condition 'x - y > 0 && x == y' is always 'false'">x - y > 0 && <warning descr="Condition 'x == y' is always 'false' when reached">x == y</warning></warning>) {}
+    if (y > 0 && x >= y) {
+      if (<warning descr="Condition 'x - y < 0' is always 'false'">x - y < 0</warning>) {}
+      if (<warning descr="Condition 'x - y > 0 && x == y' is always 'false'">x - y > 0 && <warning descr="Condition 'x == y' is always 'false' when reached">x == y</warning></warning>) {}
+    }
+    if (x > 0 && y > 0) {
+      if (<warning descr="Condition 'x - y > 1 && x <= y' is always 'false'">x - y > 1 && <warning descr="Condition 'x <= y' is always 'false' when reached">x <= y</warning></warning>) {}
+      if (x - y > -1 && x <= y) {}
+      if (x - y < -1 && <warning descr="Condition 'x <= y' is always 'true' when reached">x <= y</warning>) {}
+      if (<warning descr="Condition 'x - y == y && x == y' is always 'false'">x - y == y && <warning descr="Condition 'x == y' is always 'false' when reached">x == y</warning></warning>) {}
+      if (x - y < y && (x == y || x < y)) {}
+      if (x - y > y && (<warning descr="Condition 'x == y || x > y' is always 'true' when reached"><warning descr="Condition 'x == y' is always 'false' when reached">x == y</warning> || <warning descr="Condition 'x > y' is always 'true' when reached">x > y</warning></warning>)) {}
+    } else {
+      if (x - y > 1 && x <= y) {}
+      if (x - y > -1 && x <= y) {}
+      if (x - y < -1 && x <= y) {}
+      if (x - y == y && x == y) {}
+      if (x - y < y && (x == y || x < y)) {}
+    }
+  }
 }