Index: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
===================================================================
--- include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
+++ include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
@@ -284,6 +284,9 @@
   /// \sa shouldDisplayNotesAsEvents
   Optional<bool> DisplayNotesAsEvents;
 
+  /// \sa shouldAggressivelySimplifyRelationalComparison
+  Optional<bool> AggressiveRelationalComparisonSimplification;
+
   /// A helper function that retrieves option for a given full-qualified
   /// checker name.
   /// Options for checkers can be specified via 'analyzer-config' command-line
@@ -585,6 +588,14 @@
   /// to false when unset.
   bool shouldDisplayNotesAsEvents();
 
+  /// Returns true if SValBuilder should rearrange comparisons of symbolic
+  /// expressions which consist of a sum of a symbol and a concrete integer
+  /// into the format where symbols are on the left-hand side and the integer
+  /// is on the right. This is only done if both concrete integers are greater
+  /// than or equal to the quarter of the minimum value of the type and less
+  // than or equal to the quarter of the maximum value of that type.
+  bool shouldAggressivelySimplifyRelationalComparison();
+
 public:
   AnalyzerOptions() :
     AnalysisStoreOpt(RegionStoreModel),
Index: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
===================================================================
--- lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
+++ lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
@@ -392,3 +392,11 @@
         getBooleanOption("notes-as-events", /*Default=*/false);
   return DisplayNotesAsEvents.getValue();
 }
+
+bool AnalyzerOptions::shouldAggressivelySimplifyRelationalComparison() {
+  if (!AggressiveRelationalComparisonSimplification.hasValue())
+    AggressiveRelationalComparisonSimplification =
+      getBooleanOption("aggressive-relational-comparison-simplification",
+                       /*Default=*/false);
+  return AggressiveRelationalComparisonSimplification.getValue();
+}
Index: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -12,8 +12,10 @@
 //===----------------------------------------------------------------------===//
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
 
 using namespace clang;
@@ -307,6 +309,216 @@
   return makeNonLoc(LHS, op, *ConvertedRHS, resultTy);
 }
 
+// See if Sym is known to be within [min/4, max/4], where min and max
+// are the bounds of the symbol's integral type. With such symbols,
+// some manipulations can be performed without the risk of overflow.
+// assume() doesn't cause infinite recursion because we should be dealing
+// with simpler symbols on every recursive call.
+static bool isOverflowClampedBy4(SymbolRef Sym, ProgramStateRef State) {
+  SValBuilder &SVB = State->getStateManager().getSValBuilder();
+  BasicValueFactory &BV = SVB.getBasicValueFactory();
+
+  QualType T = Sym->getType();
+  assert(T->isSignedIntegerOrEnumerationType() &&
+         "This only works with signed integers!");
+  APSIntType AT = BV.getAPSIntType(T);
+
+  llvm::APSInt Max = AT.getMaxValue() >> 2; // Divide by 4.
+  SVal IsCappedFromAbove =
+      SVB.evalBinOpNN(State, BO_LE, nonloc::SymbolVal(Sym),
+                      nonloc::ConcreteInt(Max), SVB.getConditionType());
+  if (auto DV = IsCappedFromAbove.getAs<DefinedSVal>()) {
+    if (State->assume(*DV, false))
+      return false;
+  } else {
+    return false;
+  }
+
+  llvm::APSInt Min = -Max;
+  SVal IsCappedFromBelow =
+      SVB.evalBinOpNN(State, BO_GE, nonloc::SymbolVal(Sym),
+                      nonloc::ConcreteInt(Min), SVB.getConditionType());
+  if (auto DV = IsCappedFromBelow.getAs<DefinedSVal>()) {
+    if (State->assume(*DV, false))
+      return false;
+  } else {
+    return false;
+  }
+
+  return true;
+}
+
+// Same for the concrete integers: see if I is within [min/4, max/4].
+static bool isOverflowClampedBy4(llvm::APSInt I) {
+  APSIntType AT(I);
+  assert(!AT.isUnsigned() &&
+         "This only works with signed integers!");
+
+  llvm::APSInt Max = AT.getMaxValue() >> 2;
+  if (I > Max)
+    return false;
+
+  llvm::APSInt Min = -Max;
+  if (I < Min)
+    return false;
+
+  return true;
+}
+
+std::tuple<SymbolRef, BinaryOperator::Opcode, llvm::APSInt>
+decomposeSymbol(SymbolRef Sym, BasicValueFactory &BV) {
+  if (const auto *SymInt = dyn_cast<SymIntExpr>(Sym))
+    if (BinaryOperator::isAdditiveOp(SymInt->getOpcode()))
+      return std::make_tuple(SymInt->getLHS(), SymInt->getOpcode(),
+                             SymInt->getRHS());
+
+  // Fail to decompose: "reduce" the problem to the "$x + 0" case.
+  return std::make_tuple(Sym, BO_Add, BV.getValue(0, Sym->getType()));
+}
+
+// Simplify "(LSym LOp LInt) Op (RSym ROp RInt)" assuming all values are of the
+// same signed integral type and no overflows occur (which should be checked
+// by the caller).
+static NonLoc doRearrangeUnchecked(ProgramStateRef State,
+                                   BinaryOperator::Opcode Op,
+                                   SymbolRef LSym, BinaryOperator::Opcode LOp,
+                                   llvm::APSInt LInt,
+                                   SymbolRef RSym, BinaryOperator::Opcode ROp,
+                                   llvm::APSInt RInt) {
+  SValBuilder &SVB = State->getStateManager().getSValBuilder();
+  BasicValueFactory &BV = SVB.getBasicValueFactory();
+  SymbolManager &SymMgr = SVB.getSymbolManager();
+
+  QualType SymTy = LSym->getType();
+  assert(SymTy == RSym->getType() &&
+         "Symbols are not of the same type!");
+  assert(APSIntType(LInt) == BV.getAPSIntType(SymTy) &&
+         "Integers are not of the same type as symbols!");
+  assert(APSIntType(RInt) == BV.getAPSIntType(SymTy) &&
+         "Integers are not of the same type as symbols!");
+
+  // Change "$x - a" into "$x + (-a)". We'd bring back this cosmetic difference
+  // after we're done with our operations.
+  if (LOp == BO_Sub)
+    LInt = -LInt;
+  else
+    assert(LOp == BO_Add && "Unexpected operation!");
+  if (ROp == BO_Sub)
+    RInt = -RInt;
+  else
+    assert(ROp == BO_Add && "Unexpected operation!");
+
+  QualType ResultTy;
+  if (BinaryOperator::isComparisonOp(Op))
+    ResultTy = SVB.getConditionType();
+  else if (BinaryOperator::isAdditiveOp(Op))
+    ResultTy = SymTy;
+  else
+    llvm_unreachable("Operation not suitable for unchecked rearrangement!");
+
+  // FIXME: Can we use assume() without getting into an infinite recursion?
+  if (LSym == RSym)
+    return SVB.evalBinOpNN(State, Op, nonloc::ConcreteInt(LInt),
+                           nonloc::ConcreteInt(RInt), ResultTy)
+        .castAs<NonLoc>();
+
+  SymbolRef ResultSym = nullptr;
+  BinaryOperator::Opcode ResultOp;
+  llvm::APSInt ResultInt;
+  if (BinaryOperator::isComparisonOp(Op)) {
+    // Prefer comparing to a non-negative number.
+    // FIXME: Maybe it'd be better to have consistency in
+    // "$x - $y" vs. "$y - $x" because those are solver's keys.
+    if (LInt > RInt) {
+      ResultSym = SymMgr.getSymSymExpr(RSym, BO_Sub, LSym, SymTy);
+      ResultOp = BinaryOperator::reverseComparisonOp(Op);
+      ResultInt = LInt - RInt; // Opposite order!
+    } else {
+      ResultSym = SymMgr.getSymSymExpr(LSym, BO_Sub, RSym, SymTy);
+      ResultOp = Op;
+      ResultInt = RInt - LInt; // Opposite order!
+    }
+  } else {
+    ResultSym = SymMgr.getSymSymExpr(LSym, Op, RSym, SymTy);
+    ResultInt = (Op == BO_Add) ? (LInt + RInt) : (LInt - RInt);
+    ResultOp = BO_Add;
+    // Bring back the cosmetic difference.
+    if (ResultInt < 0) {
+      ResultInt = -ResultInt;
+      ResultOp = BO_Sub;
+    } else if (ResultInt == 0) {
+      // Shortcut: Simplify "$x + 0" to "$x".
+      return nonloc::SymbolVal(ResultSym);
+    }
+  }
+  const llvm::APSInt &PersistentResultInt = BV.getValue(ResultInt);
+  return nonloc::SymbolVal(
+      SymMgr.getSymIntExpr(ResultSym, ResultOp, PersistentResultInt, ResultTy));
+}
+
+static Optional<NonLoc> tryRearrange(ProgramStateRef State,
+                                     BinaryOperator::Opcode Op, NonLoc Lhs,
+                                     NonLoc Rhs, QualType ResultTy) {
+  ProgramStateManager &StateMgr = State->getStateManager();
+  SValBuilder &SVB = StateMgr.getSValBuilder();
+
+  // We expect everything to be of the same type - this type.
+  QualType SingleTy;
+
+  auto &Opts =
+    StateMgr.getOwningEngine()->getAnalysisManager().getAnalyzerOptions();
+
+  if (BinaryOperator::isComparisonOp(Op) &&
+      Opts.shouldAggressivelySimplifyRelationalComparison()) {
+    if (ResultTy != SVB.getConditionType())
+      return None;
+    // Initialize SingleTy later with a symbol's type.
+  } else if (BinaryOperator::isAdditiveOp(Op)) {
+    SingleTy = ResultTy;
+  } else {
+    // Don't rearrange other operations.
+    return None;
+  }
+
+  SymbolRef LSym = Lhs.getAsSymbol();
+  if (!LSym)
+    return None;
+
+  if (BinaryOperator::isAdditiveOp(Op)) {
+    if (SingleTy != ResultTy)
+      return None;
+  } else {
+    SingleTy = LSym->getType();
+  }
+
+  assert(!SingleTy.isNull() && "We should have figured out the type by now!");
+
+  // Substracting unsigned integers is a nightmare.
+  if (!SingleTy->isSignedIntegerOrEnumerationType())
+    return None;
+
+  SymbolRef RSym = Rhs.getAsSymbol();
+  if (!RSym || RSym->getType() != SingleTy)
+    return None;
+
+  BasicValueFactory &BV = State->getBasicVals();
+  llvm::APSInt LInt, RInt;
+  BinaryOperator::Opcode LOp, ROp;
+  std::tie(LSym, LOp, LInt) = decomposeSymbol(LSym, BV);
+  if (LSym->getType() != SingleTy ||
+      !isOverflowClampedBy4(LSym, State) || !isOverflowClampedBy4(LInt))
+    return None;
+
+  std::tie(RSym, ROp, RInt) = decomposeSymbol(RSym, BV);
+  if (RSym->getType() != SingleTy ||
+      (BinaryOperator::isComparisonOp(Op) &&
+       (!isOverflowClampedBy4(RSym, State) || !isOverflowClampedBy4(RInt))))
+    return None;
+
+  // We know that no overflows can occur anymore.
+  return doRearrangeUnchecked(State, Op, LSym, LOp, LInt, RSym, ROp, RInt);
+}
+
 SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
                                   BinaryOperator::Opcode op,
                                   NonLoc lhs, NonLoc rhs,
@@ -559,6 +771,9 @@
       if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
         return MakeSymIntVal(Sym, op, *RHSValue, resultTy);
 
+      if (Optional<NonLoc> V = tryRearrange(state, op, lhs, rhs, resultTy))
+        return *V;
+
       // Give up -- this is not a symbolic expression we can handle.
       return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy);
     }
Index: test/Analysis/svalbuilder-rearrange-comparisons.c
===================================================================
--- /dev/null
+++ test/Analysis/svalbuilder-rearrange-comparisons.c
@@ -0,0 +1,927 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+
+void clang_analyzer_dump(int x);
+void clang_analyzer_eval(int x);
+
+void exit(int);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+
+int g();
+int f() {
+  int x = g();
+  // Assert that no overflows occur in this test file.
+  // Assuming that concrete integers are also within that range.
+  if (x > ((int)INT_MAX / 4))
+    exit(1);
+  if (x < -(((int)INT_MAX) / 4))
+    exit(1);
+  return x;
+}
+
+void compare_different_symbol_equal() {
+  int x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int_equal() {
+  int x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int_equal() {
+  int x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int_equal() {
+  int x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int_equal() {
+  int x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_equal() {
+  int x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_equal() {
+  int x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_equal() {
+  int x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_equal() {
+  int x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_same_symbol_equal() {
+  int x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_equal() {
+  int x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_int_equal() {
+  int x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_right_int_equal() {
+  int x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_right_int_equal() {
+  int x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_equal() {
+  int x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_equal() {
+  int x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_equal() {
+  int x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_equal() {
+  int x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_different_symbol_less_or_equal() {
+  int x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_or_equal() {
+  int x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_or_equal() {
+  int x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_or_equal() {
+  int x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_or_equal() {
+  int x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_or_equal() {
+  int x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_or_equal() {
+  int x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_or_equal() {
+  int x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_or_equal() {
+  int x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 1}}
+}
+
+void compare_same_symbol_less_or_equal() {
+  int x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_less_or_equal() {
+  int x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_int_less_or_equal() {
+  int x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_right_int_less_or_equal() {
+  int x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_minus_right_int_less_or_equal() {
+  int x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_or_equal() {
+  int x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_or_equal() {
+  int x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_or_equal() {
+  int x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_or_equal() {
+  int x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_different_symbol_less() {
+  int x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 0}}
+}
+
+void compare_different_symbol_plus_left_int_less() {
+  int x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_minus_left_int_less() {
+  int x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 1}}
+}
+
+void compare_different_symbol_plus_right_int_less() {
+  int x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 2}}
+}
+
+void compare_different_symbol_minus_right_int_less() {
+  int x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less() {
+  int x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less() {
+  int x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less() {
+  int x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less() {
+  int x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 1}}
+}
+
+void compare_same_symbol_less() {
+  int x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_less() {
+  int x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_int_less() {
+  int x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_right_int_less() {
+  int x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_minus_right_int_less() {
+  int x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less() {
+  int x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less() {
+  int x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less() {
+  int x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less() {
+  int x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_different_symbol_equal_unsigned() {
+  unsigned x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int_equal_unsigned() {
+  unsigned x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int_equal_unsigned() {
+  unsigned x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_same_symbol_equal_unsigned() {
+  unsigned x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_equal_unsigned() {
+  unsigned x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_equal_unsigned() {
+  unsigned x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_different_symbol_less_or_equal_unsigned() {
+  unsigned x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_or_equal_unsigned() {
+  unsigned x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_or_equal_unsigned() {
+  unsigned x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) >= 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) <= 1}}
+}
+
+void compare_same_symbol_less_or_equal_unsigned() {
+  unsigned x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{1 S32b}}
+}
+
+void compare_different_symbol_less_unsigned() {
+  unsigned x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_unsigned() {
+  unsigned x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_unsigned() {
+  unsigned x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_unsigned() {
+  unsigned x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_unsigned() {
+  unsigned x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) > 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_unsigned() {
+  unsigned x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_unsigned() {
+  unsigned x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) < 1}}
+}
+
+void compare_same_symbol_less_unsigned() {
+  unsigned x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_int_less_unsigned() {
+  unsigned x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_less_unsigned() {
+  unsigned x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{0 S32b}}
+}
+
+void overflow(signed char n, signed char m) {
+  if (n + 0 > m + 0) {
+    clang_analyzer_eval(n - 126 == m + 3); // expected-warning{{UNKNOWN}}
+  }
+}