// RUN: %clang_analyze_cc1 %s \
// RUN:   -analyzer-checker=core \
// RUN:   -analyzer-checker=debug.ExprInspection \
// RUN:   -verify

// In this test we check whether the solver's symbol simplification mechanism
// is capable of reaching a fixpoint.

void clang_analyzer_warnIfReached();

void test_contradiction(int a, int b, int c, int d, int x) {
  if (a + b + c != d)
    return;
  if (a == d)
    return;
  if (b + c != 0)
    return;
  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}

  // Bring in the contradiction.
  if (b != 0)
    return;

  // After the simplification of `b == 0` we have:
  //   b == 0
  //   a + c == d
  //   a != d
  //   c == 0
  // Doing another iteration we reach the fixpoint (with a contradiction):
  //   b == 0
  //   a == d
  //   a != d
  //   c == 0
  clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE

  // Enabling expensive checks would trigger an assertion failure here without
  // the fixpoint iteration.
  if (a + c == x)
    return;

  // Keep the symbols and the constraints! alive.
  (void)(a * b * c * d * x);
  return;
}

void test_true_range_contradiction(int a, unsigned b) {
  if (!(b > a))   // unsigned b > int a
    return;
  if (a != -1)    // int a == -1
    return;       // Starts a simplification of `unsigned b > int a`,
                  // that results in `unsigned b > UINT_MAX`,
                  // which is always false, so the State is infeasible.
  clang_analyzer_warnIfReached(); // no-warning
  (void)(a * b);
}