Method min_trailing_ones

smt/expr.cpp:658–663

}

unsigned expr::min_trailing_ones() const {
  uint64_t n;
  if (isUInt(n))
    return countr_one(n);
  return 0;
}

expr expr::binop_commutative(const expr &rhs,
                             Z3_ast (*op)(Z3_context, Z3_ast, Z3_ast),