1 (bvsmod s t) abbreviates 2 (let (?msb_s (extract[|m-1|:|m-1|] s)) 3 (let (?msb_t (extract[|m-1|:|m-1|] t)) 4 (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) 5 (bvurem s t) 6 (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) 7 (bvadd (bvneg (bvurem (bvneg s) t)) t) 8 (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) 9 (bvadd (bvurem s (bvneg t)) t) 10 (bvneg (bvurem (bvneg s) (bvneg t)))))))) 11