; (bv[0] = 1) => (bv + (2^32-1))[31:1] = bv[31:1]

(=>
(= {bitsel [bitvec 32 bv] 0 0} {bitconst 1})
(= {bitsel {bitplus bv -1 {bitconst 1}} 31 1}
   {bitsel bv 31 1}))