Method ule

smt/expr.cpp:1722–1733

}

expr expr::ule(const expr &rhs) const {
  if (eq(rhs) || isZero() || rhs.isAllOnes())
    return true;
  if (rhs.isZero() || isAllOnes())
    return *this == rhs;

  // 00... <= ..111 -> true
  if (min_leading_zeros() + rhs.min_trailing_ones() >= bits())
    return true;

  return binop_fold(rhs, Z3_mk_bvule);
}

expr expr::ult(const expr &rhs) const {
  C();