Method fshr

smt/expr.cpp:961–966

}

expr expr::fshr(const expr &a, const expr &b, const expr &c) {
  C2(a);
  auto width = mkUInt(a.bits(), a.sort());
  expr c_mod_width = c.urem(width);
  return a << (width - c_mod_width) | b.lshr(c_mod_width);
}

/*
 * FIXME: the fixed point functions are allowed to round towards zero