text: // RUN: %clang_analyze_cc1 %s \
  // RUN:   -analyzer-checker=core \
  // RUN:   -analyzer-checker=debug.ExprInspection \
  // RUN:   -analyzer-config eagerly-assume=false \
  // RUN:   -verify
  
  void clang_analyzer_eval(bool);
  void clang_analyzer_warnIfReached();
  
  int test_legacy_behavior(int x, int y) {
    if (y != 0)
      return 0;
    if (x + y != 0)
      return 0;
    clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
    clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
    return y / (x + y);              // expected-warning{{Division by zero}}
  }
  
  int test_rhs_further_constrained(int x, int y) {
    if (x + y != 0)
      return 0;
    if (y != 0)
      return 0;
    clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
    clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
    return 0;
  }
  
  int test_lhs_further_constrained(int x, int y) {
    if (x + y != 0)
      return 0;
    if (x != 0)
      return 0;
    clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
    clang_analyzer_eval(x == 0);     // expected-warning{{TRUE}}
    return 0;
  }
  
  int test_lhs_and_rhs_further_constrained(int x, int y) {
    if (x % y != 1)
      return 0;
    if (x != 1)
      return 0;
    if (y != 2)
      return 0;
    clang_analyzer_eval(x % y == 1); // expected-warning{{TRUE}}
    clang_analyzer_eval(y == 2);     // expected-warning{{TRUE}}
    return 0;
  }
  
  int test_commutativity(int x, int y) {
    if (x + y != 0)
      return 0;
    if (y != 0)
      return 0;
    clang_analyzer_eval(y + x == 0); // expected-warning{{TRUE}}
    clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
    return 0;
  }
  
  int test_binop_when_height_is_2_r(int a, int x, int y, int z) {
    switch (a) {
    case 1: {
      if (x + y + z != 0)
        return 0;
      if (z != 0)
        return 0;
      clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
      clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}}
      break;
    }
    case 2: {
      if (x + y + z != 0)
        return 0;
      if (y != 0)
        return 0;
      clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
      clang_analyzer_eval(y == 0);         // expected-warning{{TRUE}}
      break;
    }
    case 3: {
      if (x + y + z != 0)
        return 0;
      if (x != 0)
        return 0;
      clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
      clang_analyzer_eval(x == 0);         // expected-warning{{TRUE}}
      break;
    }
    case 4: {
      if (x + y + z != 0)
        return 0;
      if (x + y != 0)
        return 0;
      clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
      clang_analyzer_eval(x + y == 0);     // expected-warning{{TRUE}}
      break;
    }
    case 5: {
      if (z != 0)
        return 0;
      if (x + y + z != 0)
        return 0;
      clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
      if (y != 0)
        return 0;
      clang_analyzer_eval(y == 0);         // expected-warning{{TRUE}}
      clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}}
      clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
      break;
    }
  
    }
    return 0;
  }
  
  void test_equivalence_classes_are_updated(int a, int b, int c, int d) {
    if (a + b != c)
      return;
    if (a != d)
      return;
    if (b != 0)
      return;
    clang_analyzer_eval(c == d); // expected-warning{{TRUE}}
    // Keep the symbols and the constraints! alive.
    (void)(a * b * c * d);
    return;
  }
  
  void test_contradiction(int a, int b, int c, int d) {
    if (a + b != c)
      return;
    if (a == c)
      return;
    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
  
    // Bring in the contradiction.
    if (b != 0)
      return;
    clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE
    // Keep the symbols and the constraints! alive.
    (void)(a * b * c * d);
    return;
  }
  
  void test_deferred_contradiction(int e0, int b0, int b1) {
  
    int e1 = e0 - b0; // e1 is bound to (reg_$0<int e0>) - (reg_$1<int b0>)
    (void)(b0 == 2);  // bifurcate
  
    int e2 = e1 - b1;
    if (e2 > 0) { // b1 != e1
      clang_analyzer_warnIfReached();   // expected-warning{{REACHABLE}}
      // Here, e1 is still bound to (reg_$0<int e0>) - (reg_$1<int b0>) but we
      // should be able to simplify it to (reg_$0<int e0>) - 2 and thus realize
      // the contradiction.
      if (b1 == e1) {
        clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE
        (void)(b0 * b1 * e0 * e1 * e2);
      }
    }
  }
  