private boolean applyBinOpRelations(DfaValue left, RelationType type, DfaValue right) {
    if (type != RelationType.LT && type != RelationType.GT && type != RelationType.NE && type != RelationType.EQ) return true;
    if (!(left instanceof DfaBinOpValue binOp)) {
      if (right instanceof DfaBinOpValue) {
        return applyBinOpRelations(right, type.getFlipped(), left);
      }
      return true;
    }
    LongRangeBinOp op = binOp.getOperation();
    if (op != LongRangeBinOp.PLUS && op != LongRangeBinOp.MINUS) return true;
    DfaVariableValue leftLeft = binOp.getLeft();
    DfaValue leftRight = binOp.getRight();
    LongRangeSet leftRange = extractRange(getDfType(leftLeft));
    LongRangeSet rightRange = extractRange(getDfType(leftRight));
    LongRangeType lrType = binOp.getDfType().getLongRangeType();
    LongRangeSet rightNegated = rightRange.negate(lrType);
    LongRangeSet rightCorrected = op == LongRangeBinOp.MINUS ? rightNegated : rightRange;

    LongRangeSet resultRange = extractRange(getDfType(right));
    RelationType correctedRelation = correctRelation(type, leftRange, rightCorrected, resultRange, lrType);
    if (op == LongRangeBinOp.MINUS) {
      long min = resultRange.min();
      long max = resultRange.max();
      if (min == 0 && max == 0) {
        // a-b (rel) 0 => a (rel) b
        if (!applyCondition(leftLeft.cond(correctedRelation, leftRight))) return false;
      }
      else if (min == 0 && type == RelationType.GT || min >= 1 && RelationType.GE.isSubRelation(type)) {
        RelationType correctedGt = correctRelation(RelationType.GT, leftRange, rightCorrected, resultRange, lrType);
        if (!applyCondition(leftLeft.cond(correctedGt, leftRight))) return false;
      }
      else if (max == 0 && type == RelationType.LT || max <= -1 && RelationType.LE.isSubRelation(type)) {
        RelationType correctedLt = correctRelation(RelationType.LT, leftRange, rightCorrected, resultRange, lrType);
        if (!applyCondition(leftLeft.cond(correctedLt, leftRight))) return false;
      }
      if (RelationType.EQ.equals(type) && !resultRange.contains(0)) {
        // a-b == non-zero => a != b
        if (!applyRelation(leftLeft, leftRight, true)) return false;
      }
    }
    if (op == LongRangeBinOp.PLUS && RelationType.EQ == type &&
        !resultRange.intersects(lrType.fullRange().mul(LongRangeSet.point(2), lrType))) {
      // a+b == odd => a != b
      if (!applyRelation(leftLeft, leftRight, true)) return false;
    }
    if (right instanceof DfaVariableValue) {
      // a+b (rel) c && a == c => b (rel) 0
      if (areEqual(leftLeft, right)) {
        RelationType finalRelation = op == LongRangeBinOp.MINUS ?
                                     Objects.requireNonNull(correctedRelation.getFlipped()) : correctedRelation;
        if (!applyCondition(leftRight.cond(finalRelation, binOp.getDfType().meetRange(LongRangeSet.point(0))))) return false;
      }
      // a+b (rel) c && b == c => a (rel) 0
      if (op == LongRangeBinOp.PLUS && areEqual(leftRight, right)) {
        if (!applyCondition(leftLeft.cond(correctedRelation, binOp.getDfType().meetRange(LongRangeSet.point(0))))) return false;
      }

      if (!applyRelationOnAddition(type, leftLeft, leftRange, rightCorrected, right, lrType)) return false;
      if (op == LongRangeBinOp.PLUS && leftRight instanceof DfaVariableValue) {
        if (!applyRelationOnAddition(type, (DfaVariableValue)leftRight, rightRange, leftRange, right, lrType)) return false;
      }
    }
    return true;
  }
private boolean applyBinOpRelations(DfaValue left, RelationType type, DfaValue right)