Create BitVec arithmetic shift right (bvashr) expression. The shifted expressions is padded with sign (leftmost, highest) bits.
bvashr