(bvashr s t) abbreviates 
      (ite (= (extract[|m-1|:|m-1|] s) bit0)
           (bvlshr s t)
           (bvnot (bvlshr (bvnot s) t)))