; (PC[0] = 0) => (PC[31:1] + 1) << 1 = PC + 2

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