Method lshr

smt/expr.cpp:938–952

}

expr expr::lshr(const expr &rhs) const {
  C();
  if (isZero() || rhs.isZero())
    return *this;

  uint64_t shift;
  if (rhs.isUInt(shift)) {
    auto bw = bits();
    if (shift >= bw)
      return mkUInt(0, sort());
    return mkUInt(0, shift).concat(extract(bw-1, shift));
  }

  return binop_fold(rhs, Z3_mk_bvlshr);
}

expr expr::fshl(const expr &a, const expr &b, const expr &c) {
  C2(a);