Method ugt

smt/expr.cpp:1748–1759

}

expr expr::ugt(const expr &rhs) const {
  C();
  if (rhs.isAllOnes())
    return false;

  uint64_t n;
  if (rhs.isUInt(n)) {
    auto ty = sort();
    return uge(mkUInt(n, ty) + mkUInt(1, ty));
  }
  return !ule(rhs);
}

expr expr::sle(const expr &rhs) const {
  if (eq(rhs) || rhs.isSMax())